theorem Th100: :: INTPRO_2:99

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