# Metamath Proof Explorer

## Theorem ltletr

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

Ref Expression
Assertion ltletr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}\le {C}\right)\to {A}<{C}\right)$

### Proof

Step Hyp Ref Expression
1 leloe ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}\le {C}↔\left({B}<{C}\vee {B}={C}\right)\right)$
2 1 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}\le {C}↔\left({B}<{C}\vee {B}={C}\right)\right)$
3 lttr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}<{C}\right)\to {A}<{C}\right)$
4 3 expcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}<{C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
5 breq2 ${⊢}{B}={C}\to \left({A}<{B}↔{A}<{C}\right)$
6 5 biimpd ${⊢}{B}={C}\to \left({A}<{B}\to {A}<{C}\right)$
7 6 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}={C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
8 4 7 jaod ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({B}<{C}\vee {B}={C}\right)\to \left({A}<{B}\to {A}<{C}\right)\right)$
9 2 8 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}\le {C}\to \left({A}<{B}\to {A}<{C}\right)\right)$
10 9 impcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\wedge {B}\le {C}\right)\to {A}<{C}\right)$