theorem Th72: :: INTPRO_2:71

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