# 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 ${⊢}{\phi }\to \left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)$
lelttrdi.l ${⊢}{\phi }\to {B}\le {C}$
Assertion lelttrdi ${⊢}{\phi }\to \left({A}<{B}\to {A}<{C}\right)$

### Proof

Step Hyp Ref Expression
1 lelttrdi.r ${⊢}{\phi }\to \left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)$
2 lelttrdi.l ${⊢}{\phi }\to {B}\le {C}$
3 1 simp1d ${⊢}{\phi }\to {A}\in ℝ$
4 3 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {A}\in ℝ$
5 1 simp2d ${⊢}{\phi }\to {B}\in ℝ$
6 5 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {B}\in ℝ$
7 1 simp3d ${⊢}{\phi }\to {C}\in ℝ$
8 7 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {C}\in ℝ$
9 simpr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {A}<{B}$
10 2 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {B}\le {C}$
11 4 6 8 9 10 ltletrd ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {A}<{C}$
12 11 ex ${⊢}{\phi }\to \left({A}<{B}\to {A}<{C}\right)$