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