theorem :: INTPRO_2:164

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