Theorem lttrd 11296

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 11211	. . 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 11026   < clt 11168

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 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-pre-lttrn 11102

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 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  mulgt1  12006  nnne0  12200  neglt  12951  expgt1  14051  ltexp2a  14117  expcan  14120  ltexp2  14121  leexp2  14122  expnlbnd2  14185  expmulnbnd  14186  reccn2  15548  efgt1  16072  tanhlt1  16116  ruclem2  16188  isprm7  16667  pythagtriplem13  16787  fldivp1  16857  4sqlem12  16916  chnub  18577  chnccat  18581  sylow1lem1  19562  telgsums  19957  chfacffsupp  22829  chfacfscmul0  22831  chfacfpmmul0  22835  nrginvrcnlem  24664  iccntr  24795  icccmplem2  24797  opnreen  24805  pjthlem1  25412  pmltpclem2  25424  ovollb2lem  25463  opnmbllem  25576  volivth  25582  lhop1lem  25988  dvcnvrelem1  25992  dvcvx  25995  ftc1lem4  26014  aaliou3lem7  26324  ulmdvlem1  26376  reeff1olem  26422  pilem2  26428  pilem3  26429  tangtx  26480  tanord1  26512  tanord  26513  rplogcl  26579  logimul  26589  logcnlem3  26619  efopnlem1  26631  cxplt  26669  cxple  26670  cxpcn3lem  26722  asinsin  26867  atanlogaddlem  26888  atanlogsublem  26890  cxp2limlem  26951  cxp2lim  26952  zetacvg  26990  lgamucov  27013  lgamcvg2  27030  ftalem1  27048  mersenne  27202  bposlem2  27260  bposlem6  27264  bposlem9  27267  lgsqrlem2  27322  lgsquadlem2  27356  chebbnd1lem2  27445  chebbnd1lem3  27446  chebbnd1  27447  chtppilimlem1  27448  chto1ub  27451  mulog2sumlem2  27510  chpdifbndlem1  27528  selberg3lem1  27532  pntrlog2bndlem2  27553  pntrlog2bndlem4  27555  pntpbnd1a  27560  pntpbnd1  27561  pntpbnd2  27562  pntibndlem1  27564  pntibndlem2  27566  pntibndlem3  27567  pntibnd  27568  pntlemb  27572  pntlemr  27577  pntlemf  27580  pnt  27589  ostth2lem1  27593  ostth2lem3  27610  ostth2lem4  27611  wwlksext2clwwlk  30140  frgrogt3nreg  30480  friendshipgt3  30481  pjhthlem1  31475  sgnsub  32923  psgnfzto1stlem  33174  1smat1  33962  sqsscirc1  34066  xrge0iifiso  34093  signslema  34720  chtvalz  34787  hgt750lemd  34806  knoppndvlem12  36789  knoppndvlem14  36791  knoppndvlem15  36792  knoppndvlem17  36794  knoppndvlem20  36797  poimirlem6  37951  poimirlem7  37952  poimirlem8  37953  poimirlem15  37960  poimirlem20  37965  poimirlem28  37973  opnmbllem0  37981  itg2gt0cn  38000  ftc1cnnclem  38016  ftc1anc  38026  cntotbnd  38121  3lexlogpow5ineq3  42500  3lexlogpow2ineq2  42502  3lexlogpow5ineq5  42503  aks4d1lem1  42505  0nonelalab  42510  aks4d1p1p3  42512  aks4d1p1p2  42513  aks4d1p1p4  42514  aks4d1p1p6  42516  aks4d1p1p7  42517  aks4d1p1p5  42518  aks4d1p1  42519  aks4d1p2  42520  aks4d1p3  42521  aks4d1p6  42524  aks4d1p7d1  42525  aks4d1p7  42526  aks4d1p8d3  42529  aks4d1p8  42530  2ap1caineq  42588  sticksstones1  42589  sn-addlt0d  42907  sn-addgt0d  42908  sn-mulgt1d  42928  fimgmcyc  42983  flt4lem7  43096  fltnlta  43100  pellexlem5  43269  pellfundex  43322  pellfundrp  43324  rmspecfund  43345  monotuz  43377  jm3.1lem2  43454  jm3.1lem3  43455  imo72b2  44607  prmunb2  44746  ltadd12dd  45781  infleinflem2  45808  sqrlearg  45991  lptre2pt  46076  0ellimcdiv  46085  limsup10exlem  46208  ioodvbdlimc1lem1  46367  iblspltprt  46409  itgspltprt  46415  stoweidlem7  46443  stoweidlem11  46447  stoweidlem13  46449  stoweidlem14  46450  stoweidlem26  46462  stoweidlem42  46478  stoweidlem52  46488  stoweidlem59  46495  stoweidlem60  46496  stoweidlem62  46498  wallispilem4  46504  wallispi  46506  stirlinglem1  46510  stirlinglem3  46512  stirlinglem6  46515  stirlinglem7  46516  stirlinglem10  46519  stirlinglem11  46520  dirkercncflem1  46539  dirkercncflem2  46540  fourierdlem10  46553  fourierdlem11  46554  fourierdlem12  46555  fourierdlem42  46585  fourierdlem47  46589  fourierdlem50  46592  fourierdlem51  46593  fourierdlem73  46615  fourierdlem79  46621  fourierdlem83  46625  fourierdlem103  46645  fourierdlem104  46646  sqwvfoura  46664  sqwvfourb  46665  fouriersw  46667  hoidmvlelem1  47031  hoiqssbllem2  47059  hspmbllem1  47062  pimrecltpos  47144  pimrecltneg  47160  smfaddlem1  47199  smflimlem3  47209  smflimlem4  47210  smfmullem1  47227  ormkglobd  47311  chnsubseq  47316  difmodm1lt  47815  2timesltsqm1  47829  fpprel2  48219  gpgedgvtx0  48539  gpgedgvtx1  48540  eenglngeehlnmlem2  49216