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