theorem Th25: :: INTPRO_2:24

for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds X |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by INTPRO_1:8;