theorem :: INTPRO_2:158

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