theorem Th106: :: INTPRO_2:105

for p, q being Element of MC-wff holds |-_IPC (p => q) => (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))