Theorem lttrd 11422

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  mulgt1  12129  nnne0  12300  expgt1  14141  ltexp2a  14206  expcan  14209  ltexp2  14210  leexp2  14211  expnlbnd2  14273  expmulnbnd  14274  reccn2  15633  efgt1  16152  tanhlt1  16196  ruclem2  16268  isprm7  16745  pythagtriplem13  16865  fldivp1  16935  4sqlem12  16994  sylow1lem1  19616  telgsums  20011  chfacffsupp  22862  chfacfscmul0  22864  chfacfpmmul0  22868  nrginvrcnlem  24712  iccntr  24843  icccmplem2  24845  opnreen  24853  pjthlem1  25471  pmltpclem2  25484  ovollb2lem  25523  opnmbllem  25636  volivth  25642  lhop1lem  26052  dvcnvrelem1  26056  dvcvx  26059  ftc1lem4  26080  aaliou3lem7  26391  ulmdvlem1  26443  reeff1olem  26490  pilem2  26496  pilem3  26497  tangtx  26547  tanord1  26579  tanord  26580  rplogcl  26646  logimul  26656  logcnlem3  26686  efopnlem1  26698  cxplt  26736  cxple  26737  cxpcn3lem  26790  asinsin  26935  atanlogaddlem  26956  atanlogsublem  26958  cxp2limlem  27019  cxp2lim  27020  zetacvg  27058  lgamucov  27081  lgamcvg2  27098  ftalem1  27116  mersenne  27271  bposlem2  27329  bposlem6  27333  bposlem9  27336  lgsqrlem2  27391  lgsquadlem2  27425  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chto1ub  27520  mulog2sumlem2  27579  chpdifbndlem1  27597  selberg3lem1  27601  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem1  27633  pntibndlem2  27635  pntibndlem3  27636  pntibnd  27637  pntlemb  27641  pntlemr  27646  pntlemf  27649  pnt  27658  ostth2lem1  27662  ostth2lem3  27679  ostth2lem4  27680  wwlksext2clwwlk  30076  frgrogt3nreg  30416  friendshipgt3  30417  pjhthlem1  31410  chnub  33002  psgnfzto1stlem  33120  1smat1  33803  sqsscirc1  33907  xrge0iifiso  33934  sgnsub  34547  signslema  34577  chtvalz  34644  hgt750lemd  34663  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem20  36532  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem15  37642  poimirlem20  37647  poimirlem28  37655  opnmbllem0  37663  itg2gt0cn  37682  ftc1cnnclem  37698  ftc1anc  37708  cntotbnd  37803  3lexlogpow5ineq3  42058  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  0nonelalab  42068  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8d3  42087  aks4d1p8  42088  2ap1caineq  42146  sticksstones1  42147  sn-addlt0d  42476  sn-addgt0d  42477  sn-mulgt1d  42495  fimgmcyc  42544  flt4lem7  42669  fltnlta  42673  pellexlem5  42844  pellfundex  42897  pellfundrp  42899  rmspecfund  42920  monotuz  42953  jm3.1lem2  43030  jm3.1lem3  43031  imo72b2  44185  prmunb2  44330  neglt  45296  ltadd12dd  45354  infleinflem2  45382  sqrlearg  45566  lptre2pt  45655  0ellimcdiv  45664  limsup10exlem  45787  ioodvbdlimc1lem1  45946  iblspltprt  45988  itgspltprt  45994  stoweidlem7  46022  stoweidlem11  46026  stoweidlem13  46028  stoweidlem14  46029  stoweidlem26  46041  stoweidlem42  46057  stoweidlem52  46067  stoweidlem59  46074  stoweidlem60  46075  stoweidlem62  46077  wallispilem4  46083  wallispi  46085  stirlinglem1  46089  stirlinglem3  46091  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  dirkercncflem1  46118  dirkercncflem2  46119  fourierdlem10  46132  fourierdlem11  46133  fourierdlem12  46134  fourierdlem42  46164  fourierdlem47  46168  fourierdlem50  46171  fourierdlem51  46172  fourierdlem73  46194  fourierdlem79  46200  fourierdlem83  46204  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  hoidmvlelem1  46610  hoiqssbllem2  46638  hspmbllem1  46641  pimrecltpos  46723  pimrecltneg  46739  smfaddlem1  46778  smflimlem3  46788  smflimlem4  46789  smfmullem1  46806  ormkglobd  46890  fpprel2  47728  gpgedgvtx0  48019  gpgedgvtx1  48020  eenglngeehlnmlem2  48659