theorem Th19: :: INTPRO_2:18

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