Theorem lttrd 11305

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   < clt 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  mulgt1  12015  nnne0  12209  neglt  12960  expgt1  14060  ltexp2a  14126  expcan  14129  ltexp2  14130  leexp2  14131  expnlbnd2  14194  expmulnbnd  14195  reccn2  15557  efgt1  16081  tanhlt1  16125  ruclem2  16197  isprm7  16676  pythagtriplem13  16796  fldivp1  16866  4sqlem12  16925  chnub  18586  chnccat  18590  sylow1lem1  19571  telgsums  19966  chfacffsupp  22846  chfacfscmul0  22848  chfacfpmmul0  22852  nrginvrcnlem  24681  iccntr  24812  icccmplem2  24814  opnreen  24822  pjthlem1  25429  pmltpclem2  25441  ovollb2lem  25480  opnmbllem  25593  volivth  25599  lhop1lem  26005  dvcnvrelem1  26009  dvcvx  26012  ftc1lem4  26031  aaliou3lem7  26340  ulmdvlem1  26390  reeff1olem  26436  pilem2  26442  pilem3  26443  tangtx  26494  tanord1  26526  tanord  26527  rplogcl  26593  logimul  26603  logcnlem3  26633  efopnlem1  26645  cxplt  26683  cxple  26684  cxpcn3lem  26736  asinsin  26881  atanlogaddlem  26902  atanlogsublem  26904  cxp2limlem  26964  cxp2lim  26965  zetacvg  27003  lgamucov  27026  lgamcvg2  27043  ftalem1  27061  mersenne  27215  bposlem2  27273  bposlem6  27277  bposlem9  27280  lgsqrlem2  27335  lgsquadlem2  27369  chebbnd1lem2  27458  chebbnd1lem3  27459  chebbnd1  27460  chtppilimlem1  27461  chto1ub  27464  mulog2sumlem2  27523  chpdifbndlem1  27541  selberg3lem1  27545  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntibndlem1  27577  pntibndlem2  27579  pntibndlem3  27580  pntibnd  27581  pntlemb  27585  pntlemr  27590  pntlemf  27593  pnt  27602  ostth2lem1  27606  ostth2lem3  27623  ostth2lem4  27624  wwlksext2clwwlk  30152  frgrogt3nreg  30492  friendshipgt3  30493  pjhthlem1  31487  sgnsub  32936  psgnfzto1stlem  33188  1smat1  33995  sqsscirc1  34099  xrge0iifiso  34126  signslema  34753  chtvalz  34820  hgt750lemd  34839  knoppndvlem12  36836  knoppndvlem14  36838  knoppndvlem15  36839  knoppndvlem17  36841  knoppndvlem20  36844  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem15  38009  poimirlem20  38014  poimirlem28  38022  opnmbllem0  38030  itg2gt0cn  38049  ftc1cnnclem  38065  ftc1anc  38075  cntotbnd  38170  3lexlogpow5ineq3  42549  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1lem1  42554  0nonelalab  42559  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p2  42569  aks4d1p3  42570  aks4d1p6  42573  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8d3  42578  aks4d1p8  42579  2ap1caineq  42637  sticksstones1  42638  sn-addlt0d  42955  sn-addgt0d  42956  sn-mulgt1d  42976  fimgmcyc  43027  flt4lem7  43116  fltnlta  43120  pellexlem5  43285  pellfundex  43338  pellfundrp  43340  rmspecfund  43361  monotuz  43393  jm3.1lem2  43470  jm3.1lem3  43471  imo72b2  44623  prmunb2  44762  ltadd12dd  45795  infleinflem2  45822  sqrlearg  46005  lptre2pt  46090  0ellimcdiv  46099  limsup10exlem  46222  ioodvbdlimc1lem1  46381  iblspltprt  46423  itgspltprt  46429  stoweidlem7  46457  stoweidlem11  46461  stoweidlem13  46463  stoweidlem14  46464  stoweidlem26  46476  stoweidlem42  46492  stoweidlem52  46502  stoweidlem59  46509  stoweidlem60  46510  stoweidlem62  46512  wallispilem4  46518  wallispi  46520  stirlinglem1  46524  stirlinglem3  46526  stirlinglem6  46529  stirlinglem7  46530  stirlinglem10  46533  stirlinglem11  46534  dirkercncflem1  46553  dirkercncflem2  46554  fourierdlem10  46567  fourierdlem11  46568  fourierdlem12  46569  fourierdlem42  46599  fourierdlem47  46603  fourierdlem50  46606  fourierdlem51  46607  fourierdlem73  46629  fourierdlem79  46635  fourierdlem83  46639  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  hoidmvlelem1  47045  hoiqssbllem2  47073  hspmbllem1  47076  pimrecltpos  47158  pimrecltneg  47174  smfaddlem1  47213  smflimlem3  47223  smflimlem4  47224  smfmullem1  47241  ormkglobd  47327  chnsubseq  47332  difmodm1lt  47835  2timesltsqm1  47849  fpprel2  48239  gpgedgvtx0  48559  gpgedgvtx1  48560  eenglngeehlnmlem2  49236