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