theorem Th113: :: INTPRO_2:112

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