Theorem lttrd 11419

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  mulgt1  12126  nnne0  12297  expgt1  14137  ltexp2a  14202  expcan  14205  ltexp2  14206  leexp2  14207  expnlbnd2  14269  expmulnbnd  14270  reccn2  15629  efgt1  16148  tanhlt1  16192  ruclem2  16264  isprm7  16741  pythagtriplem13  16860  fldivp1  16930  4sqlem12  16989  sylow1lem1  19630  telgsums  20025  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  nrginvrcnlem  24727  iccntr  24856  icccmplem2  24858  opnreen  24866  pjthlem1  25484  pmltpclem2  25497  ovollb2lem  25536  opnmbllem  25649  volivth  25655  lhop1lem  26066  dvcnvrelem1  26070  dvcvx  26073  ftc1lem4  26094  aaliou3lem7  26405  ulmdvlem1  26457  reeff1olem  26504  pilem2  26510  pilem3  26511  tangtx  26561  tanord1  26593  tanord  26594  rplogcl  26660  logimul  26670  logcnlem3  26700  efopnlem1  26712  cxplt  26750  cxple  26751  cxpcn3lem  26804  asinsin  26949  atanlogaddlem  26970  atanlogsublem  26972  cxp2limlem  27033  cxp2lim  27034  zetacvg  27072  lgamucov  27095  lgamcvg2  27112  ftalem1  27130  mersenne  27285  bposlem2  27343  bposlem6  27347  bposlem9  27350  lgsqrlem2  27405  lgsquadlem2  27439  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chto1ub  27534  mulog2sumlem2  27593  chpdifbndlem1  27611  selberg3lem1  27615  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem1  27647  pntibndlem2  27649  pntibndlem3  27650  pntibnd  27651  pntlemb  27655  pntlemr  27660  pntlemf  27663  pnt  27672  ostth2lem1  27676  ostth2lem3  27693  ostth2lem4  27694  wwlksext2clwwlk  30085  frgrogt3nreg  30425  friendshipgt3  30426  pjhthlem1  31419  chnub  32985  psgnfzto1stlem  33102  1smat1  33764  sqsscirc1  33868  xrge0iifiso  33895  sgnsub  34525  signslema  34555  chtvalz  34622  hgt750lemd  34641  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem20  36513  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem15  37621  poimirlem20  37626  poimirlem28  37634  opnmbllem0  37642  itg2gt0cn  37661  ftc1cnnclem  37677  ftc1anc  37687  cntotbnd  37782  3lexlogpow5ineq3  42038  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  0nonelalab  42048  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d3  42067  aks4d1p8  42068  2ap1caineq  42126  sticksstones1  42127  sn-addlt0d  42452  sn-addgt0d  42453  sn-mulgt1d  42471  fimgmcyc  42520  flt4lem7  42645  fltnlta  42649  pellexlem5  42820  pellfundex  42873  pellfundrp  42875  rmspecfund  42896  monotuz  42929  jm3.1lem2  43006  jm3.1lem3  43007  imo72b2  44161  prmunb2  44306  neglt  45234  ltadd12dd  45292  infleinflem2  45320  sqrlearg  45505  lptre2pt  45595  0ellimcdiv  45604  limsup10exlem  45727  ioodvbdlimc1lem1  45886  iblspltprt  45928  itgspltprt  45934  stoweidlem7  45962  stoweidlem11  45966  stoweidlem13  45968  stoweidlem14  45969  stoweidlem26  45981  stoweidlem42  45997  stoweidlem52  46007  stoweidlem59  46014  stoweidlem60  46015  stoweidlem62  46017  wallispilem4  46023  wallispi  46025  stirlinglem1  46029  stirlinglem3  46031  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  dirkercncflem1  46058  dirkercncflem2  46059  fourierdlem10  46072  fourierdlem11  46073  fourierdlem12  46074  fourierdlem42  46104  fourierdlem47  46108  fourierdlem50  46111  fourierdlem51  46112  fourierdlem73  46134  fourierdlem79  46140  fourierdlem83  46144  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  hoidmvlelem1  46550  hoiqssbllem2  46578  hspmbllem1  46581  pimrecltpos  46663  pimrecltneg  46679  smfaddlem1  46718  smflimlem3  46728  smflimlem4  46729  smfmullem1  46746  fpprel2  47665  gpgedgvtx0  47953  gpgedgvtx1  47954  eenglngeehlnmlem2  48587