Metamath Proof Explorer

Theorem ltletr

Description: Transitive law. (Contributed by NM, 25-Aug-1999)

Ref Expression
Assertion ltletr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B∧B≤C→A<C

Proof

Step Hyp Ref Expression
1 leloe ⊢B∈ℝ∧C∈ℝ→B≤C↔B<C∨B=C
2 1 3adant1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B≤C↔B<C∨B=C
3 lttr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B∧B<C→A<C
4 3 expcomd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<C→A<B→A<C
5 breq2 ⊢B=C→A<B↔A<C
6 5 biimpd ⊢B=C→A<B→A<C
7 6 a1i ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B=C→A<B→A<C
8 4 7 jaod ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<C∨B=C→A<B→A<C
9 2 8 sylbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B≤C→A<B→A<C
10 9 impcomd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B∧B≤C→A<C