theorem :: INTPRO_2:155

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