theorem Th89: :: INTPRO_2:88

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