let p, q, s be Element of HP-WFF ; :: thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
A1: (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by Lm16;
((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by Lm17;
hence (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by A1, Th23; :: thesis: verum