Theorem lttri 11259

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

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ
lt.3	⊢ 𝐶 ∈ ℝ

Assertion

Ref	Expression
lttri	⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Proof of Theorem lttri

Step	Hyp	Ref	Expression
1		lt.1	. 2 ⊢ 𝐴 ∈ ℝ
2		lt.2	. 2 ⊢ 𝐵 ∈ ℝ
3		lt.3	. 2 ⊢ 𝐶 ∈ ℝ
4		lttr 11209	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	1, 2, 3, 4	mp3an 1463	1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttrn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171

This theorem is referenced by:  1lt3  12313  2lt4  12315  1lt4  12316  3lt5  12318  2lt5  12319  1lt5  12320  4lt6  12322  3lt6  12323  2lt6  12324  1lt6  12325  5lt7  12327  4lt7  12328  3lt7  12329  2lt7  12330  1lt7  12331  6lt8  12333  5lt8  12334  4lt8  12335  3lt8  12336  2lt8  12337  1lt8  12338  7lt9  12340  6lt9  12341  5lt9  12342  4lt9  12343  3lt9  12344  2lt9  12345  1lt9  12346  8lt10  12739  7lt10  12740  6lt10  12741  5lt10  12742  4lt10  12743  3lt10  12744  2lt10  12745  1lt10  12746  sincos2sgn  16119  epos  16132  ene1  16135  dvdslelem  16236  psgnodpmr  21545  xrhmph  24901  vitalilem4  25568  pipos  26424  logi  26552  logneg  26553  asin1  26860  reasinsin  26862  atan1  26894  log2le1  26916  bposlem8  27258  bposlem9  27259  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  mulog2sumlem2  27502  pntibndlem1  27556  pntlemb  27564  pntlemk  27573  axlowdimlem16  29030  sgnnbi  32919  sgnpbi  32920  dp2ltc  32968  signswch  34718  hgt750lem  34808  hgt750lem2  34809  cnndvlem1  36737  bj-minftyccb  37426  bj-pinftynminfty  37428  irrdiff  37527  asindmre  37900  fdc  37942  lttrii  42507  sn-0ne2  42657  fourierdlem94  46440  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  fourierdlem113  46459  fourierdlem114  46460  fouriersw  46471  etransclem23  46497