Theorem lttrd 11307

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 11222	. . 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 5085  ℝcr 11037   < clt 11179

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-pre-lttrn 11113

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 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 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  mulgt1  12017  nnne0  12211  neglt  12962  expgt1  14062  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2  14133  expnlbnd2  14196  expmulnbnd  14197  reccn2  15559  efgt1  16083  tanhlt1  16127  ruclem2  16199  isprm7  16678  pythagtriplem13  16798  fldivp1  16868  4sqlem12  16927  chnub  18588  chnccat  18592  sylow1lem1  19573  telgsums  19968  chfacffsupp  22821  chfacfscmul0  22823  chfacfpmmul0  22827  nrginvrcnlem  24656  iccntr  24787  icccmplem2  24789  opnreen  24797  pjthlem1  25404  pmltpclem2  25416  ovollb2lem  25455  opnmbllem  25568  volivth  25574  lhop1lem  25980  dvcnvrelem1  25984  dvcvx  25987  ftc1lem4  26006  aaliou3lem7  26315  ulmdvlem1  26365  reeff1olem  26411  pilem2  26417  pilem3  26418  tangtx  26469  tanord1  26501  tanord  26502  rplogcl  26568  logimul  26578  logcnlem3  26608  efopnlem1  26620  cxplt  26658  cxple  26659  cxpcn3lem  26711  asinsin  26856  atanlogaddlem  26877  atanlogsublem  26879  cxp2limlem  26939  cxp2lim  26940  zetacvg  26978  lgamucov  27001  lgamcvg2  27018  ftalem1  27036  mersenne  27190  bposlem2  27248  bposlem6  27252  bposlem9  27255  lgsqrlem2  27310  lgsquadlem2  27344  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chto1ub  27439  mulog2sumlem2  27498  chpdifbndlem1  27516  selberg3lem1  27520  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem1  27552  pntibndlem2  27554  pntibndlem3  27555  pntibnd  27556  pntlemb  27560  pntlemr  27565  pntlemf  27568  pnt  27577  ostth2lem1  27581  ostth2lem3  27598  ostth2lem4  27599  wwlksext2clwwlk  30127  frgrogt3nreg  30467  friendshipgt3  30468  pjhthlem1  31462  sgnsub  32910  psgnfzto1stlem  33161  1smat1  33948  sqsscirc1  34052  xrge0iifiso  34079  signslema  34706  chtvalz  34773  hgt750lemd  34792  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem20  36791  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem15  37956  poimirlem20  37961  poimirlem28  37969  opnmbllem0  37977  itg2gt0cn  37996  ftc1cnnclem  38012  ftc1anc  38022  cntotbnd  38117  3lexlogpow5ineq3  42496  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  0nonelalab  42506  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d3  42525  aks4d1p8  42526  2ap1caineq  42584  sticksstones1  42585  sn-addlt0d  42903  sn-addgt0d  42904  sn-mulgt1d  42924  fimgmcyc  42979  flt4lem7  43092  fltnlta  43096  pellexlem5  43261  pellfundex  43314  pellfundrp  43316  rmspecfund  43337  monotuz  43369  jm3.1lem2  43446  jm3.1lem3  43447  imo72b2  44599  prmunb2  44738  ltadd12dd  45773  infleinflem2  45800  sqrlearg  45983  lptre2pt  46068  0ellimcdiv  46077  limsup10exlem  46200  ioodvbdlimc1lem1  46359  iblspltprt  46401  itgspltprt  46407  stoweidlem7  46435  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem26  46454  stoweidlem42  46470  stoweidlem52  46480  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  wallispilem4  46496  wallispi  46498  stirlinglem1  46502  stirlinglem3  46504  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  dirkercncflem1  46531  dirkercncflem2  46532  fourierdlem10  46545  fourierdlem11  46546  fourierdlem12  46547  fourierdlem42  46577  fourierdlem47  46581  fourierdlem50  46584  fourierdlem51  46585  fourierdlem73  46607  fourierdlem79  46613  fourierdlem83  46617  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  hoidmvlelem1  47023  hoiqssbllem2  47051  hspmbllem1  47054  pimrecltpos  47136  pimrecltneg  47152  smfaddlem1  47191  smflimlem3  47201  smflimlem4  47202  smfmullem1  47219  ormkglobd  47305  chnsubseq  47310  difmodm1lt  47813  2timesltsqm1  47827  fpprel2  48217  gpgedgvtx0  48537  gpgedgvtx1  48538  eenglngeehlnmlem2  49214