theorem :: INTPRO_2:143

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