theorem :: INTPRO_2:163

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