theorem :: INTPRO_2:154

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