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

Metamath Proof Explorer

Theorem axlttrn

Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn with ordering on the extended reals. New proofs should use lttr instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion axlttrn ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ∧ B < C → A < C

Proof

Step Hyp Ref Expression
1 ax-pre-lttrn ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < ℝ B ∧ B < ℝ C → A < ℝ C
2 ltxrlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < ℝ B
3 2 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ A < ℝ B
4 ltxrlt ⊢ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ B < ℝ C
5 4 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ B < ℝ C
6 3 5 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ∧ B < C ↔ A < ℝ B ∧ B < ℝ C
7 ltxrlt ⊢ A ∈ ℝ ∧ C ∈ ℝ → A < C ↔ A < ℝ C
8 7 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ↔ A < ℝ C
9 1 6 8 3imtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ∧ B < C → A < C