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