theorem Th79: :: INTPRO_2:78

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