Theorem lttri 9760

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

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1868   class class class wbr 4420   RRcr 9538   < clt 9675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-resscn 9596  ax-pre-lttrn 9614

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-ltxr 9680

This theorem is referenced by:  1lt3  10778  2lt4  10780  1lt4  10781  3lt5  10783  2lt5  10784  1lt5  10785  4lt6  10787  3lt6  10788  2lt6  10789  1lt6  10790  5lt7  10792  4lt7  10793  3lt7  10794  2lt7  10795  1lt7  10796  6lt8  10798  5lt8  10799  4lt8  10800  3lt8  10801  2lt8  10802  1lt8  10803  7lt9  10805  6lt9  10806  5lt9  10807  4lt9  10808  3lt9  10809  2lt9  10810  1lt9  10811  8lt10  10813  7lt10  10814  6lt10  10815  5lt10  10816  4lt10  10817  3lt10  10818  2lt10  10819  1lt10  10820  sincos2sgn  14235  epos  14246  ene1  14249  dvdslelem  14336  oppcbas  15610  sralem  18387  zlmlem  19074  psgnodpmr  19144  tnglem  21634  xrhmph  21961  vitalilem4  22555  pipos  23401  logneg  23523  asin1  23806  reasinsin  23808  atan1  23840  log2le1  23862  bposlem8  24205  bposlem9  24206  chebbnd1lem2  24294  chebbnd1lem3  24295  chebbnd1  24296  mulog2sumlem2  24359  pntibndlem1  24413  pntlemb  24421  pntlemk  24430  ttglem  24892  cchhllem  24903  axlowdimlem16  24973  sgnnbi  29411  sgnpbi  29412  signswch  29445  logi  30364  bj-minftyccb  31618  bj-pinftynminfty  31620  asindmre  31940  fdc  31987  fourierdlem94  37883  fourierdlem102  37891  fourierdlem103  37892  fourierdlem104  37893  fourierdlem112  37901  fourierdlem113  37902  fourierdlem114  37903  fouriersw  37914  etransclem23  37941