theorem Th8: :: INTPRO_1:8

for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X