Theorem lttri 10163

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079

This theorem is referenced by:  1lt3  11196  2lt4  11198  1lt4  11199  3lt5  11201  2lt5  11202  1lt5  11203  4lt6  11205  3lt6  11206  2lt6  11207  1lt6  11208  5lt7  11210  4lt7  11211  3lt7  11212  2lt7  11213  1lt7  11214  6lt8  11216  5lt8  11217  4lt8  11218  3lt8  11219  2lt8  11220  1lt8  11221  7lt9  11223  6lt9  11224  5lt9  11225  4lt9  11226  3lt9  11227  2lt9  11228  1lt9  11229  8lt10OLD  11231  7lt10OLD  11232  6lt10OLD  11233  5lt10OLD  11234  4lt10OLD  11235  3lt10OLD  11236  2lt10OLD  11237  1lt10OLD  11238  8lt10  11674  7lt10  11675  6lt10  11676  5lt10  11677  4lt10  11678  3lt10  11679  2lt10  11680  1lt10  11681  sincos2sgn  14924  epos  14935  ene1  14938  dvdslelem  15031  oppcbas  16378  sralem  19177  zlmlem  19865  psgnodpmr  19936  tnglem  22444  xrhmph  22746  vitalilem4  23380  pipos  24212  logneg  24334  asin1  24621  reasinsin  24623  atan1  24655  log2le1  24677  bposlem8  25016  bposlem9  25017  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  mulog2sumlem2  25224  pntibndlem1  25278  pntlemb  25286  pntlemk  25295  ttglem  25756  cchhllem  25767  axlowdimlem16  25837  dp2ltc  29594  sgnnbi  30607  sgnpbi  30608  signswch  30638  hgt750lem  30729  hgt750lem2  30730  logi  31620  cnndvlem1  32528  bj-minftyccb  33112  bj-pinftynminfty  33114  asindmre  33495  fdc  33541  fourierdlem94  40417  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  fouriersw  40448  etransclem23  40474