theorem :: INTPRO_2:137

for p, q being Element of MC-wff holds |-_IPC (p => (neg q)) => (neg (p '&' q)) by Th88;