theorem :: INTPRO_2:142

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