Theorem lttrd 11306

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 11221	. . 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 5100  ℝcr 11037   < clt 11178

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  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 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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  mulgt1  12015  nnne0  12191  neglt  12937  expgt1  14035  ltexp2a  14101  expcan  14104  ltexp2  14105  leexp2  14106  expnlbnd2  14169  expmulnbnd  14170  reccn2  15532  efgt1  16053  tanhlt1  16097  ruclem2  16169  isprm7  16647  pythagtriplem13  16767  fldivp1  16837  4sqlem12  16896  chnub  18557  chnccat  18561  sylow1lem1  19539  telgsums  19934  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  nrginvrcnlem  24647  iccntr  24778  icccmplem2  24780  opnreen  24788  pjthlem1  25405  pmltpclem2  25418  ovollb2lem  25457  opnmbllem  25570  volivth  25576  lhop1lem  25986  dvcnvrelem1  25990  dvcvx  25993  ftc1lem4  26014  aaliou3lem7  26325  ulmdvlem1  26377  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  26725  asinsin  26870  atanlogaddlem  26891  atanlogsublem  26893  cxp2limlem  26954  cxp2lim  26955  zetacvg  26993  lgamucov  27016  lgamcvg2  27033  ftalem1  27051  mersenne  27206  bposlem2  27264  bposlem6  27268  bposlem9  27271  lgsqrlem2  27326  lgsquadlem2  27360  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chto1ub  27455  mulog2sumlem2  27514  chpdifbndlem1  27532  selberg3lem1  27536  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem1  27568  pntibndlem2  27570  pntibndlem3  27571  pntibnd  27572  pntlemb  27576  pntlemr  27581  pntlemf  27584  pnt  27593  ostth2lem1  27597  ostth2lem3  27614  ostth2lem4  27615  wwlksext2clwwlk  30144  frgrogt3nreg  30484  friendshipgt3  30485  pjhthlem1  31478  sgnsub  32928  psgnfzto1stlem  33193  1smat1  33981  sqsscirc1  34085  xrge0iifiso  34112  signslema  34739  chtvalz  34806  hgt750lemd  34825  knoppndvlem12  36742  knoppndvlem14  36744  knoppndvlem15  36745  knoppndvlem17  36747  knoppndvlem20  36750  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem15  37883  poimirlem20  37888  poimirlem28  37896  opnmbllem0  37904  itg2gt0cn  37923  ftc1cnnclem  37939  ftc1anc  37949  cntotbnd  38044  3lexlogpow5ineq3  42424  3lexlogpow2ineq2  42426  3lexlogpow5ineq5  42427  aks4d1lem1  42429  0nonelalab  42434  aks4d1p1p3  42436  aks4d1p1p2  42437  aks4d1p1p4  42438  aks4d1p1p6  42440  aks4d1p1p7  42441  aks4d1p1p5  42442  aks4d1p1  42443  aks4d1p2  42444  aks4d1p3  42445  aks4d1p6  42448  aks4d1p7d1  42449  aks4d1p7  42450  aks4d1p8d3  42453  aks4d1p8  42454  2ap1caineq  42512  sticksstones1  42513  sn-addlt0d  42825  sn-addgt0d  42826  sn-mulgt1d  42846  fimgmcyc  42901  flt4lem7  43014  fltnlta  43018  pellexlem5  43187  pellfundex  43240  pellfundrp  43242  rmspecfund  43263  monotuz  43295  jm3.1lem2  43372  jm3.1lem3  43373  imo72b2  44525  prmunb2  44664  ltadd12dd  45699  infleinflem2  45726  sqrlearg  45910  lptre2pt  45995  0ellimcdiv  46004  limsup10exlem  46127  ioodvbdlimc1lem1  46286  iblspltprt  46328  itgspltprt  46334  stoweidlem7  46362  stoweidlem11  46366  stoweidlem13  46368  stoweidlem14  46369  stoweidlem26  46381  stoweidlem42  46397  stoweidlem52  46407  stoweidlem59  46414  stoweidlem60  46415  stoweidlem62  46417  wallispilem4  46423  wallispi  46425  stirlinglem1  46429  stirlinglem3  46431  stirlinglem6  46434  stirlinglem7  46435  stirlinglem10  46438  stirlinglem11  46439  dirkercncflem1  46458  dirkercncflem2  46459  fourierdlem10  46472  fourierdlem11  46473  fourierdlem12  46474  fourierdlem42  46504  fourierdlem47  46508  fourierdlem50  46511  fourierdlem51  46512  fourierdlem73  46534  fourierdlem79  46540  fourierdlem83  46544  fourierdlem103  46564  fourierdlem104  46565  sqwvfoura  46583  sqwvfourb  46584  fouriersw  46586  hoidmvlelem1  46950  hoiqssbllem2  46978  hspmbllem1  46981  pimrecltpos  47063  pimrecltneg  47079  smfaddlem1  47118  smflimlem3  47128  smflimlem4  47129  smfmullem1  47146  ormkglobd  47230  chnsubseq  47235  difmodm1lt  47716  fpprel2  48098  gpgedgvtx0  48418  gpgedgvtx1  48419  eenglngeehlnmlem2  49095