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	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A A

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cr	|- RR
2	0 1	wcel	|- A e. RR
3		cB	|- B
4	3 1	wcel	|- B e. RR
5		cC	|- C
6	5 1	wcel	|- C e. RR
7	2 4 6	w3a	|- ( A e. RR /\ B e. RR /\ C e. RR )
8		cltrr	|-
9	0 3 8	wbr	|- A
10	3 5 8	wbr	|- B
11	9 10	wa	|- ( A
12	0 5 8	wbr	|- A
13	11 12	wi	|- ( ( A A
14	7 13	wi	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A A