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)) in HP_TAUT by Th45;
A2: (s '&' p) => (p '&' s) in HP_TAUT by Th43;
((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in HP_TAUT by Th24;
then ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT by A1, Def10;
hence (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT by A2, Def10; :: thesis: verum