Theorem inscom ≪ | index | src | ≫ 

theorem inscom (a b c: nat): $ a ; b ; c = b ; a ; c $;
StepHypRefExpression
1 axext 
a ; b ; c == b ; a ; c -> a ; b ; c = b ; a ; c
2 elins 
x e. a ; b ; c <-> x = a \/ x e. b ; c
3 elins 
x e. b ; a ; c <-> x = b \/ x e. a ; c
4 oreq2 
(x e. b ; c <-> x = b \/ x e. c) -> (x = a \/ x e. b ; c <-> x = a \/ (x = b \/ x e. c))
5 elins 
x e. b ; c <-> x = b \/ x e. c
6 4, 5 ax_mp 
x = a \/ x e. b ; c <-> x = a \/ (x = b \/ x e. c)
7 oreq2 
(x e. a ; c <-> x = a \/ x e. c) -> (x = b \/ x e. a ; c <-> x = b \/ (x = a \/ x e. c))
8 elins 
x e. a ; c <-> x = a \/ x e. c
9 7, 8 ax_mp 
x = b \/ x e. a ; c <-> x = b \/ (x = a \/ x e. c)
10 or12 
x = a \/ (x = b \/ x e. c) <-> x = b \/ (x = a \/ x e. c)
11 6, 9, 10 bitr4gi 
x = a \/ x e. b ; c <-> x = b \/ x e. a ; c
12 2, 3, 11 bitr4gi 
x e. a ; b ; c <-> x e. b ; a ; c
13 12 ax_gen 
A. x (x e. a ; b ; c <-> x e. b ; a ; c)
14 13 conv eqs 
a ; b ; c == b ; a ; c
15 1, 14 ax_mp 
a ; b ; c = b ; a ; c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)