theorem :: INTPRO_2:145

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