theorem :: INTPRO_2:134

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