let p, q, s be Element of HP-WFF ; :: thesis: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40;
(p => q) => ((p '&' s) => q) in HP_TAUT by Th39;
hence (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th23; :: thesis: verum