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