Theorem lttri 9488

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1755   class class class wbr 4280   RRcr 9269   < clt 9406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-pre-lttrn 9345

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-ltxr 9411

This theorem is referenced by:  1lt3  10478  2lt4  10480  1lt4  10481  3lt5  10483  2lt5  10484  1lt5  10485  4lt6  10487  3lt6  10488  2lt6  10489  1lt6  10490  5lt7  10492  4lt7  10493  3lt7  10494  2lt7  10495  1lt7  10496  6lt8  10498  5lt8  10499  4lt8  10500  3lt8  10501  2lt8  10502  1lt8  10503  7lt9  10505  6lt9  10506  5lt9  10507  4lt9  10508  3lt9  10509  2lt9  10510  1lt9  10511  8lt10  10513  7lt10  10514  6lt10  10515  5lt10  10516  4lt10  10517  3lt10  10518  2lt10  10519  1lt10  10520  sincos2sgn  13461  epos  13472  dvdslelem  13560  oppcbas  14640  sralem  17180  zlmlem  17790  psgnodpmr  17862  tnglem  20068  xrhmph  20361  vitalilem4  20933  pipos  21808  logneg  21921  asin1  22174  reasinsin  22176  atan1  22208  bposlem8  22515  bposlem9  22516  chebbnd1lem2  22604  chebbnd1lem3  22605  chebbnd1  22606  mulog2sumlem2  22669  pntibndlem1  22723  pntlemb  22731  pntlemk  22740  ttglem  22945  cchhllem  22956  axlowdimlem16  23026  log2le1  26320  sgnnbi  26776  sgnpbi  26777  signswch  26810  asindmre  28323  fdc  28485  ene1  30818  bj-minftyccb  32128  bj-pinftynminfty  32130