theorem :: INTPRO_2:138

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