theorem Th93: :: INTPRO_2:92

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