theorem Th94: :: INTPRO_2:93

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