Theorem lttri 8124

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 8093	. 2 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
5	1, 2, 3, 4	mp3an 1348	1 |- ( ( A < B /\ B < C ) -> A < C )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164   class class class wbr 4029   RRcr 7871   < clt 8054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-pre-lttrn 7986

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-pnf 8056  df-mnf 8057  df-ltxr 8059

This theorem is referenced by:  1lt3  9153  2lt4  9155  1lt4  9156  3lt5  9158  2lt5  9159  1lt5  9160  4lt6  9162  3lt6  9163  2lt6  9164  1lt6  9165  5lt7  9167  4lt7  9168  3lt7  9169  2lt7  9170  1lt7  9171  6lt8  9173  5lt8  9174  4lt8  9175  3lt8  9176  2lt8  9177  1lt8  9178  7lt9  9180  6lt9  9181  5lt9  9182  4lt9  9183  3lt9  9184  2lt9  9185  1lt9  9186  8lt10  9579  7lt10  9580  6lt10  9581  5lt10  9582  4lt10  9583  3lt10  9584  2lt10  9585  1lt10  9586  sincos2sgn  11909  cos12dec  11911  epos  11924  ene1  11928  eap1  11929  reeff1o  14908  pipos  14923  pigt3  14979  apdiff  15538