theorem Th128: :: INTPRO_2:127

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