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