theorem :: PL_AXIOM:45

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