let p, q, s be Element of MC-wff ; :: thesis: (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut
set P = p 'or' s;
set Q = q 'or' s;
A1: (p 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Def14;
p => (p 'or' s) in IPC-Taut by Def14;
then p => (q 'or' (p 'or' s)) in IPC-Taut by A1, Th26;
then A2: ((q 'or' (p 'or' s)) 'or' p) => ((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) => (q 'or' (p 'or' s)) in IPC-Taut by Th54;
then A3: ((q 'or' (p 'or' s)) 'or' p) => (q 'or' (p 'or' s)) in IPC-Taut by A2, Th26;
s => (p 'or' s) in IPC-Taut by Def14;
then (q 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Th63;
then A4: (p 'or' (q 'or' s)) => (p 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
(p 'or' (q 'or' (p 'or' s))) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by Th56;
then (p 'or' (q 'or' s)) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by A4, Th26;
hence (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut by A3, Th26; :: thesis: verum