Theorem lttrd 11295

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 11210	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027   < clt 11168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-pre-lttrn 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  mulgt1  12004  nnne0  12180  neglt  12931  expgt1  14025  ltexp2a  14091  expcan  14094  ltexp2  14095  leexp2  14096  expnlbnd2  14159  expmulnbnd  14160  reccn2  15522  efgt1  16043  tanhlt1  16087  ruclem2  16159  isprm7  16637  pythagtriplem13  16757  fldivp1  16827  4sqlem12  16886  sylow1lem1  19495  telgsums  19890  chfacffsupp  22759  chfacfscmul0  22761  chfacfpmmul0  22765  nrginvrcnlem  24595  iccntr  24726  icccmplem2  24728  opnreen  24736  pjthlem1  25353  pmltpclem2  25366  ovollb2lem  25405  opnmbllem  25518  volivth  25524  lhop1lem  25934  dvcnvrelem1  25938  dvcvx  25941  ftc1lem4  25962  aaliou3lem7  26273  ulmdvlem1  26325  reeff1olem  26372  pilem2  26378  pilem3  26379  tangtx  26430  tanord1  26462  tanord  26463  rplogcl  26529  logimul  26539  logcnlem3  26569  efopnlem1  26581  cxplt  26619  cxple  26620  cxpcn3lem  26673  asinsin  26818  atanlogaddlem  26839  atanlogsublem  26841  cxp2limlem  26902  cxp2lim  26903  zetacvg  26941  lgamucov  26964  lgamcvg2  26981  ftalem1  26999  mersenne  27154  bposlem2  27212  bposlem6  27216  bposlem9  27219  lgsqrlem2  27274  lgsquadlem2  27308  chebbnd1lem2  27397  chebbnd1lem3  27398  chebbnd1  27399  chtppilimlem1  27400  chto1ub  27403  mulog2sumlem2  27462  chpdifbndlem1  27480  selberg3lem1  27484  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntibndlem1  27516  pntibndlem2  27518  pntibndlem3  27519  pntibnd  27520  pntlemb  27524  pntlemr  27529  pntlemf  27532  pnt  27541  ostth2lem1  27545  ostth2lem3  27562  ostth2lem4  27563  wwlksext2clwwlk  30019  frgrogt3nreg  30359  friendshipgt3  30360  pjhthlem1  31353  sgnsub  32795  chnub  32967  psgnfzto1stlem  33055  1smat1  33773  sqsscirc1  33877  xrge0iifiso  33904  signslema  34532  chtvalz  34599  hgt750lemd  34618  knoppndvlem12  36499  knoppndvlem14  36501  knoppndvlem15  36502  knoppndvlem17  36504  knoppndvlem20  36507  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem15  37617  poimirlem20  37622  poimirlem28  37630  opnmbllem0  37638  itg2gt0cn  37657  ftc1cnnclem  37673  ftc1anc  37683  cntotbnd  37778  3lexlogpow5ineq3  42033  3lexlogpow2ineq2  42035  3lexlogpow5ineq5  42036  aks4d1lem1  42038  0nonelalab  42043  aks4d1p1p3  42045  aks4d1p1p2  42046  aks4d1p1p4  42047  aks4d1p1p6  42049  aks4d1p1p7  42050  aks4d1p1p5  42051  aks4d1p1  42052  aks4d1p2  42053  aks4d1p3  42054  aks4d1p6  42057  aks4d1p7d1  42058  aks4d1p7  42059  aks4d1p8d3  42062  aks4d1p8  42063  2ap1caineq  42121  sticksstones1  42122  sn-addlt0d  42434  sn-addgt0d  42435  sn-mulgt1d  42455  fimgmcyc  42510  flt4lem7  42635  fltnlta  42639  pellexlem5  42809  pellfundex  42862  pellfundrp  42864  rmspecfund  42885  monotuz  42917  jm3.1lem2  42994  jm3.1lem3  42995  imo72b2  44148  prmunb2  44287  ltadd12dd  45326  infleinflem2  45354  sqrlearg  45538  lptre2pt  45625  0ellimcdiv  45634  limsup10exlem  45757  ioodvbdlimc1lem1  45916  iblspltprt  45958  itgspltprt  45964  stoweidlem7  45992  stoweidlem11  45996  stoweidlem13  45998  stoweidlem14  45999  stoweidlem26  46011  stoweidlem42  46027  stoweidlem52  46037  stoweidlem59  46044  stoweidlem60  46045  stoweidlem62  46047  wallispilem4  46053  wallispi  46055  stirlinglem1  46059  stirlinglem3  46061  stirlinglem6  46064  stirlinglem7  46065  stirlinglem10  46068  stirlinglem11  46069  dirkercncflem1  46088  dirkercncflem2  46089  fourierdlem10  46102  fourierdlem11  46103  fourierdlem12  46104  fourierdlem42  46134  fourierdlem47  46138  fourierdlem50  46141  fourierdlem51  46142  fourierdlem73  46164  fourierdlem79  46170  fourierdlem83  46174  fourierdlem103  46194  fourierdlem104  46195  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  hoidmvlelem1  46580  hoiqssbllem2  46608  hspmbllem1  46611  pimrecltpos  46693  pimrecltneg  46709  smfaddlem1  46748  smflimlem3  46758  smflimlem4  46759  smfmullem1  46776  ormkglobd  46860  difmodm1lt  47347  fpprel2  47729  gpgedgvtx0  48049  gpgedgvtx1  48050  eenglngeehlnmlem2  48727