This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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