theorem Th16: :: PL_AXIOM:29

for p, q, r being Element of PL-WFF holds (p => (q => r)) => ((p => q) => (p => r)) is tautology