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