theorem Th88: :: INTPRO_2:87

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