theorem Th77: :: INTPRO_2:76

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