Theorem lttri 11416

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 11366	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	1, 2, 3, 4	mp3an 1461	1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329

This theorem is referenced by:  1lt3  12466  2lt4  12468  1lt4  12469  3lt5  12471  2lt5  12472  1lt5  12473  4lt6  12475  3lt6  12476  2lt6  12477  1lt6  12478  5lt7  12480  4lt7  12481  3lt7  12482  2lt7  12483  1lt7  12484  6lt8  12486  5lt8  12487  4lt8  12488  3lt8  12489  2lt8  12490  1lt8  12491  7lt9  12493  6lt9  12494  5lt9  12495  4lt9  12496  3lt9  12497  2lt9  12498  1lt9  12499  8lt10  12890  7lt10  12891  6lt10  12892  5lt10  12893  4lt10  12894  3lt10  12895  2lt10  12896  1lt10  12897  sincos2sgn  16242  epos  16255  ene1  16258  dvdslelem  16357  oppcbasOLD  17778  sralemOLD  21199  zlmlemOLD  21551  psgnodpmr  21631  tnglemOLD  24675  xrhmph  24997  vitalilem4  25665  pipos  26520  logi  26647  logneg  26648  asin1  26955  reasinsin  26957  atan1  26989  log2le1  27011  bposlem8  27353  bposlem9  27354  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  mulog2sumlem2  27597  pntibndlem1  27651  pntlemb  27659  pntlemk  27668  ttglemOLD  28904  cchhllemOLD  28920  axlowdimlem16  28990  dp2ltc  32851  sgnnbi  34510  sgnpbi  34511  signswch  34538  hgt750lem  34628  hgt750lem2  34629  cnndvlem1  36503  bj-minftyccb  37191  bj-pinftynminfty  37193  irrdiff  37292  asindmre  37663  fdc  37705  lttrii  42251  sn-0ne2  42382  fourierdlem94  46121  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  fourierdlem114  46141  fouriersw  46152  etransclem23  46178