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	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C)$

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 (A \in ℝ \land B \in ℝ \land C \in ℝ)$
8		cltrr	$class <_{ℝ}$
9	0 3 8	wbr	$wff A <_{ℝ} B$
10	3 5 8	wbr	$wff B <_{ℝ} C$
11	9 10	wa	$wff (A <_{ℝ} B \land B <_{ℝ} C)$
12	0 5 8	wbr	$wff A <_{ℝ} C$
13	11 12	wi	$wff ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C)$
14	7 13	wi	$wff ((A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C))$

Metamath Proof Explorer

Axiom ax-pre-lttrn

Detailed syntax breakdown