theorem :: INTPRO_1:50

for p, q, s being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut