Metamath Proof Explorer


Theorem xrltletrd

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*
xrltletrd.4 φA<B
xrltletrd.5 φBC
Assertion xrltletrd φA<C

Proof

Step Hyp Ref Expression
1 xrlttrd.1 φA*
2 xrlttrd.2 φB*
3 xrlttrd.3 φC*
4 xrltletrd.4 φA<B
5 xrltletrd.5 φBC
6 xrltletr A*B*C*A<BBCA<C
7 1 2 3 6 syl3anc φA<BBCA<C
8 4 5 7 mp2and φA<C