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