# Metamath Proof Explorer

## Theorem lelttr

Description: Transitive law. (Contributed by NM, 23-May-1999)

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

### Proof

Step Hyp Ref Expression
1 leloe ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}↔\left({A}<{B}\vee {A}={B}\right)\right)$
2 1 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {B}↔\left({A}<{B}\vee {A}={B}\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 expd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}<{B}\to \left({B}<{C}\to {A}<{C}\right)\right)$
5 breq1 ${⊢}{A}={B}\to \left({A}<{C}↔{B}<{C}\right)$
6 5 biimprd ${⊢}{A}={B}\to \left({B}<{C}\to {A}<{C}\right)$
7 6 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}={B}\to \left({B}<{C}\to {A}<{C}\right)\right)$
8 4 7 jaod ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}<{B}\vee {A}={B}\right)\to \left({B}<{C}\to {A}<{C}\right)\right)$
9 2 8 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {B}\to \left({B}<{C}\to {A}<{C}\right)\right)$
10 9 impd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}\le {B}\wedge {B}<{C}\right)\to {A}<{C}\right)$