theorem :: INTPRO_2:131

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