Theorem lttrd 11367

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095   < clt 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-pre-lttrn 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-ltxr 11244

This theorem is referenced by:  mulgt1  12072  nnne0  12266  neglt  13032  expgt1  14132  ltexp2a  14198  expcan  14201  ltexp2  14202  leexp2  14203  expnlbnd2  14266  expmulnbnd  14267  sgnsub  15139  reccn2  15644  efgt1  16168  tanhlt1  16212  ruclem2  16284  isprm7  16763  pythagtriplem13  16883  fldivp1  16953  4sqlem12  17012  chnub  18674  chnccat  18678  sylow1lem1  19664  telgsums  20059  chfacffsupp  22978  chfacfscmul0  22980  chfacfpmmul0  22984  nrginvrcnlem  24813  iccntr  24944  icccmplem2  24946  opnreen  24954  pjthlem1  25561  pmltpclem2  25573  ovollb2lem  25612  opnmbllem  25725  volivth  25731  lhop1lem  26137  dvcnvrelem1  26141  dvcvx  26144  ftc1lem4  26163  aaliou3lem7  26475  ulmdvlem1  26525  reeff1olem  26571  pilem2  26577  pilem3  26578  tangtx  26632  tanord1  26664  tanord  26665  rplogcl  26731  logimul  26741  logcnlem3  26771  efopnlem1  26783  cxplt  26821  cxple  26822  cxpcn3lem  26874  asinsin  27019  atanlogaddlem  27040  atanlogsublem  27042  cxp2limlem  27102  cxp2lim  27103  zetacvg  27141  lgamucov  27164  lgamcvg2  27181  ftalem1  27199  mersenne  27353  bposlem2  27411  bposlem6  27415  bposlem9  27418  lgsqrlem2  27473  lgsquadlem2  27507  chebbnd1lem2  27596  chebbnd1lem3  27597  chebbnd1  27598  chtppilimlem1  27599  chto1ub  27602  mulog2sumlem2  27661  chpdifbndlem1  27679  selberg3lem1  27683  pntrlog2bndlem2  27704  pntrlog2bndlem4  27706  pntpbnd1a  27711  pntpbnd1  27712  pntpbnd2  27713  pntibndlem1  27715  pntibndlem2  27717  pntibndlem3  27718  pntibnd  27719  pntlemb  27723  pntlemr  27728  pntlemf  27731  pnt  27740  ostth2lem1  27744  ostth2lem3  27761  ostth2lem4  27762  wwlksext2clwwlk  30345  frgrogt3nreg  30685  friendshipgt3  30686  pjhthlem1  31680  psgnfzto1stlem  33357  1smat1  34135  sqsscirc1  34239  xrge0iifiso  34266  signslema  34890  chtvalz  34957  hgt750lemd  34976  knoppndvlem12  36997  knoppndvlem14  36999  knoppndvlem15  37000  knoppndvlem17  37002  knoppndvlem20  37005  poimirlem6  38160  poimirlem7  38161  poimirlem8  38162  poimirlem15  38169  poimirlem20  38174  poimirlem28  38182  opnmbllem0  38190  itg2gt0cn  38209  ftc1cnnclem  38225  ftc1anc  38235  cntotbnd  38330  3lexlogpow5ineq3  42709  3lexlogpow2ineq2  42711  3lexlogpow5ineq5  42712  aks4d1lem1  42714  0nonelalab  42719  aks4d1p1p3  42721  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p2  42729  aks4d1p3  42730  aks4d1p6  42733  aks4d1p7d1  42734  aks4d1p7  42735  aks4d1p8d3  42738  aks4d1p8  42739  2ap1caineq  42797  sticksstones1  42798  sn-addlt0d  43115  sn-addgt0d  43116  sn-mulgt1d  43136  fimgmcyc  43187  flt4lem7  43276  fltnlta  43280  pellexlem5  43445  pellfundex  43498  pellfundrp  43500  rmspecfund  43521  monotuz  43553  jm3.1lem2  43630  jm3.1lem3  43631  imo72b2  44783  prmunb2  44906  ltadd12dd  45944  infleinflem2  45971  sqrlearg  46154  lptre2pt  46239  0ellimcdiv  46248  limsup10exlem  46371  ioodvbdlimc1lem1  46530  iblspltprt  46572  itgspltprt  46578  stoweidlem7  46606  stoweidlem11  46610  stoweidlem13  46612  stoweidlem14  46613  stoweidlem26  46625  stoweidlem42  46641  stoweidlem52  46651  stoweidlem59  46658  stoweidlem60  46659  stoweidlem62  46661  wallispilem4  46667  wallispi  46669  stirlinglem1  46673  stirlinglem3  46675  stirlinglem6  46678  stirlinglem7  46679  stirlinglem10  46682  stirlinglem11  46683  dirkercncflem1  46702  dirkercncflem2  46703  fourierdlem10  46716  fourierdlem11  46717  fourierdlem12  46718  fourierdlem42  46748  fourierdlem47  46752  fourierdlem50  46755  fourierdlem51  46756  fourierdlem73  46778  fourierdlem79  46784  fourierdlem83  46788  fourierdlem103  46808  fourierdlem104  46809  sqwvfoura  46827  sqwvfourb  46828  fouriersw  46830  hoidmvlelem1  47194  hoiqssbllem2  47222  hspmbllem1  47225  pimrecltpos  47307  pimrecltneg  47323  smfaddlem1  47362  smflimlem3  47372  smflimlem4  47373  smfmullem1  47390  ormkglobd  47476  chnsubseq  47481  difmodm1lt  47984  2timesltsqm1  47998  fpprel2  48388  gpgedgvtx0  48708  gpgedgvtx1  48709  eenglngeehlnmlem2  49396