theorem :: INTPRO_1:65

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