theorem Th40: :: INTPRO_2:39

for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) is valid_IPC