Theorem orass ≪ | index | src | ≫ 

theorem orass (a b c: wff): $ a \/ b \/ c <-> a \/ (b \/ c) $;
StepHypRefExpression
1 bitr 
(a \/ b \/ c <-> c \/ (a \/ b)) -> (c \/ (a \/ b) <-> a \/ (b \/ c)) -> (a \/ b \/ c <-> a \/ (b \/ c))
2 orcomb 
a \/ b \/ c <-> c \/ (a \/ b)
3 1, 2 ax_mp 
(c \/ (a \/ b) <-> a \/ (b \/ c)) -> (a \/ b \/ c <-> a \/ (b \/ c))
4 bitr 
(c \/ (a \/ b) <-> a \/ (c \/ b)) -> (a \/ (c \/ b) <-> a \/ (b \/ c)) -> (c \/ (a \/ b) <-> a \/ (b \/ c))
5 or12 
c \/ (a \/ b) <-> a \/ (c \/ b)
6 4, 5 ax_mp 
(a \/ (c \/ b) <-> a \/ (b \/ c)) -> (c \/ (a \/ b) <-> a \/ (b \/ c))
7 oreq2 
(c \/ b <-> b \/ c) -> (a \/ (c \/ b) <-> a \/ (b \/ c))
8 orcomb 
c \/ b <-> b \/ c
9 7, 8 ax_mp 
a \/ (c \/ b) <-> a \/ (b \/ c)
10 6, 9 ax_mp 
c \/ (a \/ b) <-> a \/ (b \/ c)
11 3, 10 ax_mp 
a \/ b \/ c <-> a \/ (b \/ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)