theorem or4 (a b c d: wff): $ a \/ b \/ (c \/ d) <-> a \/ c \/ (b \/ d) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
bitr4 |
(a \/ b \/ (c \/ d) <-> a \/ (b \/ (c \/ d))) -> (a \/ c \/ (b \/ d) <-> a \/ (b \/ (c \/ d))) -> (a \/ b \/ (c \/ d) <-> a \/ c \/ (b \/ d)) |
| 2 |
|
orass |
a \/ b \/ (c \/ d) <-> a \/ (b \/ (c \/ d)) |
| 3 |
1, 2 |
ax_mp |
(a \/ c \/ (b \/ d) <-> a \/ (b \/ (c \/ d))) -> (a \/ b \/ (c \/ d) <-> a \/ c \/ (b \/ d)) |
| 4 |
|
bitr4 |
(a \/ c \/ (b \/ d) <-> a \/ (c \/ (b \/ d))) -> (a \/ (b \/ (c \/ d)) <-> a \/ (c \/ (b \/ d))) -> (a \/ c \/ (b \/ d) <-> a \/ (b \/ (c \/ d))) |
| 5 |
|
orass |
a \/ c \/ (b \/ d) <-> a \/ (c \/ (b \/ d)) |
| 6 |
4, 5 |
ax_mp |
(a \/ (b \/ (c \/ d)) <-> a \/ (c \/ (b \/ d))) -> (a \/ c \/ (b \/ d) <-> a \/ (b \/ (c \/ d))) |
| 7 |
|
oreq2 |
(b \/ (c \/ d) <-> c \/ (b \/ d)) -> (a \/ (b \/ (c \/ d)) <-> a \/ (c \/ (b \/ d))) |
| 8 |
|
or12 |
b \/ (c \/ d) <-> c \/ (b \/ d) |
| 9 |
7, 8 |
ax_mp |
a \/ (b \/ (c \/ d)) <-> a \/ (c \/ (b \/ d)) |
| 10 |
6, 9 |
ax_mp |
a \/ c \/ (b \/ d) <-> a \/ (b \/ (c \/ d)) |
| 11 |
3, 10 |
ax_mp |
a \/ b \/ (c \/ d) <-> a \/ c \/ (b \/ d) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)