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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cr
2 0 1 wcel 𝐴 ∈ ℝ
3 cB 𝐵
4 3 1 wcel 𝐵 ∈ ℝ
5 cC 𝐶
6 5 1 wcel 𝐶 ∈ ℝ
7 2 4 6 w3a ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ )
8 cltrr <
9 0 3 8 wbr 𝐴 < 𝐵
10 3 5 8 wbr 𝐵 < 𝐶
11 9 10 wa ( 𝐴 < 𝐵𝐵 < 𝐶 )
12 0 5 8 wbr 𝐴 < 𝐶
13 11 12 wi ( ( 𝐴 < 𝐵𝐵 < 𝐶 ) → 𝐴 < 𝐶 )
14 7 13 wi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )