theorem :: INTPRO_2:139

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