Theorem letrd ≪ | index | src | ≫ 

theorem letrd (G: wff) (a b c: nat):
  $ G -> a <= b $ >
  $ G -> b <= c $ >
  $ G -> a <= c $;
StepHypRefExpression
1 hyp h1 
G -> a <= b
2 hyp h2 
G -> b <= c
3 2 anwl 
G /\ a + x = b -> b <= c
4 addeq2 
z = x + y -> a + z = a + (x + y)
5 4 eqeq1d 
z = x + y -> (a + z = c <-> a + (x + y) = c)
6 5 iexe 
a + (x + y) = c -> E. z a + z = c
7 6 conv le 
a + (x + y) = c -> a <= c
8 addass 
a + x + y = a + (x + y)
9 anlr 
G /\ a + x = b /\ b + y = c -> a + x = b
10 9 addeq1d 
G /\ a + x = b /\ b + y = c -> a + x + y = b + y
11 anr 
G /\ a + x = b /\ b + y = c -> b + y = c
12 10, 11 eqtrd 
G /\ a + x = b /\ b + y = c -> a + x + y = c
13 8, 12 syl5eqr 
G /\ a + x = b /\ b + y = c -> a + (x + y) = c
14 7, 13 syl 
G /\ a + x = b /\ b + y = c -> a <= c
15 14 eexda 
G /\ a + x = b -> E. y b + y = c -> a <= c
16 15 conv le 
G /\ a + x = b -> b <= c -> a <= c
17 3, 16 mpd 
G /\ a + x = b -> a <= c
18 17 eexda 
G -> E. x a + x = b -> a <= c
19 18 conv le 
G -> a <= b -> a <= c
20 1, 19 mpd 
G -> 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_peano (peano2, peano5, addeq, add0, addS)