Metamath Proof Explorer


Theorem lelttrdi

Description: If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018)

Ref Expression
Hypotheses lelttrdi.r φ A B C
lelttrdi.l φ B C
Assertion lelttrdi φ A < B A < C

Proof

Step Hyp Ref Expression
1 lelttrdi.r φ A B C
2 lelttrdi.l φ B C
3 1 simp1d φ A
4 3 adantr φ A < B A
5 1 simp2d φ B
6 5 adantr φ A < B B
7 1 simp3d φ C
8 7 adantr φ A < B C
9 simpr φ A < B A < B
10 2 adantr φ A < B B C
11 4 6 8 9 10 ltletrd φ A < B A < C
12 11 ex φ A < B A < C