theorem Th102: :: INTPRO_2:101

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