theorem Th81: :: INTPRO_2:80

for p, q being Element of MC-wff holds |-_IPC (p => q) => ((q => FALSUM) => (p => FALSUM)) by Th69, INTPRO_1:24;