theorem :: INTPRO_2:144

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