let p, q, s be Element of MC-wff ; :: thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) 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)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in IPC-Taut by Th44;
hence ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut by A1, Def14; :: thesis: verum