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

Proof

Step Hyp Ref Expression
1 ax-pre-lttrn 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A  A
2 ltxrlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A
3 2 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> A
4 ltxrlt 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B < C <-> B
5 4 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C <-> B
6 3 5 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) <-> ( A
7 ltxrlt 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A < C <-> A
8 7 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < C <-> A
9 1 6 8 3imtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )