Metamath Proof Explorer


Theorem xrletrd

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

Ref Expression
Hypotheses xrlttrd.1 φ A *
xrlttrd.2 φ B *
xrlttrd.3 φ C *
xrletrd.4 φ A B
xrletrd.5 φ B C
Assertion xrletrd φ A C

Proof

Step Hyp Ref Expression
1 xrlttrd.1 φ A *
2 xrlttrd.2 φ B *
3 xrlttrd.3 φ C *
4 xrletrd.4 φ A B
5 xrletrd.5 φ B C
6 xrletr A * B * C * A B B C A C
7 1 2 3 6 syl3anc φ A B B C A C
8 4 5 7 mp2and φ A C