let p, q, s be Element of HP-WFF ; :: thesis: (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
set T = s '&' p;
A1: ((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in HP_TAUT by Th24;
(p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by Th45;
then A2: ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT by A1, Def10;
(s '&' p) => (p '&' s) in HP_TAUT by Th43;
hence (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT by A2, Def10; :: thesis: verum