theorem th5: :: PL_AXIOM:7

for p, q, r being boolean object holds (p => q) => ((p => r) => (p => (q '&' r))) = TRUE