theorem Th104: :: INTPRO_2:103

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