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