Theorem lttrd 11298

Description: Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
lttrd.4	⊢ (𝜑 → 𝐴 < 𝐵)
lttrd.5	⊢ (𝜑 → 𝐵 < 𝐶)

Assertion

Ref	Expression
lttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lttrd

Step	Hyp	Ref	Expression
1		lttrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		lttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lttr 11213	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 700	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  mulgt1  12008  nnne0  12202  neglt  12953  expgt1  14053  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2  14124  expnlbnd2  14187  expmulnbnd  14188  reccn2  15550  efgt1  16074  tanhlt1  16118  ruclem2  16190  isprm7  16669  pythagtriplem13  16789  fldivp1  16859  4sqlem12  16918  chnub  18579  chnccat  18583  sylow1lem1  19564  telgsums  19959  chfacffsupp  22831  chfacfscmul0  22833  chfacfpmmul0  22837  nrginvrcnlem  24666  iccntr  24797  icccmplem2  24799  opnreen  24807  pjthlem1  25414  pmltpclem2  25426  ovollb2lem  25465  opnmbllem  25578  volivth  25584  lhop1lem  25990  dvcnvrelem1  25994  dvcvx  25997  ftc1lem4  26016  aaliou3lem7  26326  ulmdvlem1  26378  reeff1olem  26424  pilem2  26430  pilem3  26431  tangtx  26482  tanord1  26514  tanord  26515  rplogcl  26581  logimul  26591  logcnlem3  26621  efopnlem1  26633  cxplt  26671  cxple  26672  cxpcn3lem  26724  asinsin  26869  atanlogaddlem  26890  atanlogsublem  26892  cxp2limlem  26953  cxp2lim  26954  zetacvg  26992  lgamucov  27015  lgamcvg2  27032  ftalem1  27050  mersenne  27204  bposlem2  27262  bposlem6  27266  bposlem9  27269  lgsqrlem2  27324  lgsquadlem2  27358  chebbnd1lem2  27447  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  chto1ub  27453  mulog2sumlem2  27512  chpdifbndlem1  27530  selberg3lem1  27534  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntibndlem1  27566  pntibndlem2  27568  pntibndlem3  27569  pntibnd  27570  pntlemb  27574  pntlemr  27579  pntlemf  27582  pnt  27591  ostth2lem1  27595  ostth2lem3  27612  ostth2lem4  27613  wwlksext2clwwlk  30142  frgrogt3nreg  30482  friendshipgt3  30483  pjhthlem1  31477  sgnsub  32925  psgnfzto1stlem  33176  1smat1  33964  sqsscirc1  34068  xrge0iifiso  34095  signslema  34722  chtvalz  34789  hgt750lemd  34808  knoppndvlem12  36799  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem20  36807  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem15  37970  poimirlem20  37975  poimirlem28  37983  opnmbllem0  37991  itg2gt0cn  38010  ftc1cnnclem  38026  ftc1anc  38036  cntotbnd  38131  3lexlogpow5ineq3  42510  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  0nonelalab  42520  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d3  42539  aks4d1p8  42540  2ap1caineq  42598  sticksstones1  42599  sn-addlt0d  42917  sn-addgt0d  42918  sn-mulgt1d  42938  fimgmcyc  42993  flt4lem7  43106  fltnlta  43110  pellexlem5  43279  pellfundex  43332  pellfundrp  43334  rmspecfund  43355  monotuz  43387  jm3.1lem2  43464  jm3.1lem3  43465  imo72b2  44617  prmunb2  44756  ltadd12dd  45791  infleinflem2  45818  sqrlearg  46001  lptre2pt  46086  0ellimcdiv  46095  limsup10exlem  46218  ioodvbdlimc1lem1  46377  iblspltprt  46419  itgspltprt  46425  stoweidlem7  46453  stoweidlem11  46457  stoweidlem13  46459  stoweidlem14  46460  stoweidlem26  46472  stoweidlem42  46488  stoweidlem52  46498  stoweidlem59  46505  stoweidlem60  46506  stoweidlem62  46508  wallispilem4  46514  wallispi  46516  stirlinglem1  46520  stirlinglem3  46522  stirlinglem6  46525  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  dirkercncflem1  46549  dirkercncflem2  46550  fourierdlem10  46563  fourierdlem11  46564  fourierdlem12  46565  fourierdlem42  46595  fourierdlem47  46599  fourierdlem50  46602  fourierdlem51  46603  fourierdlem73  46625  fourierdlem79  46631  fourierdlem83  46635  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  hoidmvlelem1  47041  hoiqssbllem2  47069  hspmbllem1  47072  pimrecltpos  47154  pimrecltneg  47170  smfaddlem1  47209  smflimlem3  47219  smflimlem4  47220  smfmullem1  47237  ormkglobd  47321  chnsubseq  47326  difmodm1lt  47825  2timesltsqm1  47839  fpprel2  48229  gpgedgvtx0  48549  gpgedgvtx1  48550  eenglngeehlnmlem2  49226