let p, q, s be Element of MC-wff ; :: thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut
A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in IPC-Taut by Lm19;
(p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by Lm20;
hence (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut by A1, Th26; :: thesis: verum