theorem Th95: :: INTPRO_2:94

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