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