Metamath Proof Explorer


Theorem xrlttrd

Description: Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses xrlttrd.1
|- ( ph -> A e. RR* )
xrlttrd.2
|- ( ph -> B e. RR* )
xrlttrd.3
|- ( ph -> C e. RR* )
xrlttrd.4
|- ( ph -> A < B )
xrlttrd.5
|- ( ph -> B < C )
Assertion xrlttrd
|- ( ph -> A < C )

Proof

Step Hyp Ref Expression
1 xrlttrd.1
 |-  ( ph -> A e. RR* )
2 xrlttrd.2
 |-  ( ph -> B e. RR* )
3 xrlttrd.3
 |-  ( ph -> C e. RR* )
4 xrlttrd.4
 |-  ( ph -> A < B )
5 xrlttrd.5
 |-  ( ph -> B < C )
6 xrlttr
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> A < C ) )
7 1 2 3 6 syl3anc
 |-  ( ph -> ( ( A < B /\ B < C ) -> A < C ) )
8 4 5 7 mp2and
 |-  ( ph -> A < C )