# Metamath Proof Explorer

## Axiom ax-pre-lttrn

Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn . Note: The more general version for extended reals is axlttrn . Normally new proofs would use lttr . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-lttrn ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}{<}_{ℝ}{B}\wedge {B}{<}_{ℝ}{C}\right)\to {A}{<}_{ℝ}{C}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cr ${class}ℝ$
2 0 1 wcel ${wff}{A}\in ℝ$
3 cB ${class}{B}$
4 3 1 wcel ${wff}{B}\in ℝ$
5 cC ${class}{C}$
6 5 1 wcel ${wff}{C}\in ℝ$
7 2 4 6 w3a ${wff}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)$
8 cltrr ${class}{<}_{ℝ}$
9 0 3 8 wbr ${wff}{A}{<}_{ℝ}{B}$
10 3 5 8 wbr ${wff}{B}{<}_{ℝ}{C}$
11 9 10 wa ${wff}\left({A}{<}_{ℝ}{B}\wedge {B}{<}_{ℝ}{C}\right)$
12 0 5 8 wbr ${wff}{A}{<}_{ℝ}{C}$
13 11 12 wi ${wff}\left(\left({A}{<}_{ℝ}{B}\wedge {B}{<}_{ℝ}{C}\right)\to {A}{<}_{ℝ}{C}\right)$
14 7 13 wi ${wff}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}{<}_{ℝ}{B}\wedge {B}{<}_{ℝ}{C}\right)\to {A}{<}_{ℝ}{C}\right)\right)$