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