Theorem lttri 7994

Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
lt.1	|- A e. RR
lt.2	|- B e. RR
lt.3	|- C e. RR

Assertion

Ref	Expression
lttri	|- ( ( A < B /\ B < C ) -> A < C )

Proof of Theorem lttri

Step	Hyp	Ref	Expression
1		lt.1	. 2 |- A e. RR
2		lt.2	. 2 |- B e. RR
3		lt.3	. 2 |- C e. RR
4		lttr 7963	. 2 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
5	1, 2, 3, 4	mp3an 1326	1 |- ( ( A < B /\ B < C ) -> A < C )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2135   class class class wbr 3976   RRcr 7743   < clt 7924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-pre-lttrn 7858

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-rab 2451  df-v 2723  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-xp 4604  df-pnf 7926  df-mnf 7927  df-ltxr 7929

This theorem is referenced by:  1lt3  9019  2lt4  9021  1lt4  9022  3lt5  9024  2lt5  9025  1lt5  9026  4lt6  9028  3lt6  9029  2lt6  9030  1lt6  9031  5lt7  9033  4lt7  9034  3lt7  9035  2lt7  9036  1lt7  9037  6lt8  9039  5lt8  9040  4lt8  9041  3lt8  9042  2lt8  9043  1lt8  9044  7lt9  9046  6lt9  9047  5lt9  9048  4lt9  9049  3lt9  9050  2lt9  9051  1lt9  9052  8lt10  9444  7lt10  9445  6lt10  9446  5lt10  9447  4lt10  9448  3lt10  9449  2lt10  9450  1lt10  9451  sincos2sgn  11692  cos12dec  11694  epos  11707  ene1  11711  eap1  11712  reeff1o  13235  pipos  13250  pigt3  13306  apdiff  13761