Theorem leadd1 ≪ | index | src | ≫ 

theorem leadd1 (a b c: nat): $ a <= b <-> a + c <= b + c $;
StepHypRefExpression
1 bitr 
(a <= b <-> E. x a + x = b) -> (E. x a + x = b <-> a + c <= b + c) -> (a <= b <-> a + c <= b + c)
2 dfle 
a <= b <-> E. x a + x = b
3 1, 2 ax_mp 
(E. x a + x = b <-> a + c <= b + c) -> (a <= b <-> a + c <= b + c)
4 bitr3 
(a + x + c = b + c <-> a + x = b) -> (a + x + c = b + c <-> a + c + x = b + c) -> (a + x = b <-> a + c + x = b + c)
5 addcan1 
a + x + c = b + c <-> a + x = b
6 4, 5 ax_mp 
(a + x + c = b + c <-> a + c + x = b + c) -> (a + x = b <-> a + c + x = b + c)
7 eqeq1 
a + x + c = a + c + x -> (a + x + c = b + c <-> a + c + x = b + c)
8 addrass 
a + x + c = a + c + x
9 7, 8 ax_mp 
a + x + c = b + c <-> a + c + x = b + c
10 6, 9 ax_mp 
a + x = b <-> a + c + x = b + c
11 10 exeqi 
E. x a + x = b <-> E. x a + c + x = b + c
12 11 conv le 
E. x a + x = b <-> a + c <= b + c
13 3, 12 ax_mp 
a <= b <-> a + c <= b + 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_peano (peano2, peano5, addeq, add0, addS)