theorem Th96: :: INTPRO_2:95

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