theorem Th92: :: INTPRO_2:91

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