theorem Th127: :: INTPRO_2:126

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