let p, q, s be Element of HP-WFF ; :: thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = q '&' s;
A1: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th41;
((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT by Th34;
hence ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by A1, Def10; :: thesis: verum