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 φAB
xrletrd.5 φBC
Assertion xrletrd φAC

Proof

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