Theorem lttrd 11382

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   class class class wbr 5111  ℝcr 11110   < clt 11254

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-pre-lttrn 11186

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-ltxr 11259

This theorem is used by:  mulgt1  12087  nnne0  12281  neglt  13047  expgt1  14149  ltexp2a  14215  expcan  14218  ltexp2  14219  leexp2  14220  expnlbnd2  14283  expmulnbnd  14284  sgnsub  15162  reccn2  15667  efgt1  16189  tanhlt1  16233  ruclem2  16305  isprm7  16784  pythagtriplem13  16904  fldivp1  16974  4sqlem12  17033  chnub  18695  chnccat  18699  sylow1lem1  19691  telgsums  20086  chfacffsupp  23042  chfacfscmul0  23044  chfacfpmmul0  23048  nrginvrcnlem  24877  iccntr  25008  icccmplem2  25010  opnreen  25018  pjthlem1  25625  pmltpclem2  25637  ovollb2lem  25676  opnmbllem  25789  volivth  25795  lhop1lem  26201  dvcnvrelem1  26205  dvcvx  26208  ftc1lem4  26227  aaliou3lem7  26541  ulmdvlem1  26592  reeff1olem  26638  pilem2  26644  pilem3  26645  tangtx  26699  tanord1  26731  tanord  26732  rplogcl  26798  logimul  26808  logcnlem3  26838  efopnlem1  26850  cxplt  26888  cxple  26889  cxpcn3lem  26941  asinsin  27086  atanlogaddlem  27107  atanlogsublem  27109  cxp2limlem  27169  cxp2lim  27170  zetacvg  27208  lgamucov  27231  lgamcvg2  27248  ftalem1  27266  mersenne  27420  bposlem2  27478  bposlem6  27482  bposlem9  27485  lgsqrlem2  27540  lgsquadlem2  27574  chebbnd1lem2  27663  chebbnd1lem3  27664  chebbnd1  27665  chtppilimlem1  27666  chto1ub  27669  mulog2sumlem2  27728  chpdifbndlem1  27746  selberg3lem1  27750  pntrlog2bndlem2  27771  pntrlog2bndlem4  27773  pntpbnd1a  27778  pntpbnd1  27779  pntpbnd2  27780  pntibndlem1  27782  pntibndlem2  27784  pntibndlem3  27785  pntibnd  27786  pntlemb  27790  pntlemr  27795  pntlemf  27798  pnt  27807  ostth2lem1  27811  ostth2lem3  27828  ostth2lem4  27829  wwlksext2clwwlk  30437  frgrogt3nreg  30777  friendshipgt3  30778  pjhthlem1  31772  psgnfzto1stlem  33443  1smat1  34217  sqsscirc1  34321  xrge0iifiso  34348  signslema  34973  chtvalz  35040  hgt750lemd  35059  knoppndvlem12  37145  knoppndvlem14  37147  knoppndvlem15  37148  knoppndvlem17  37150  knoppndvlem20  37153  poimirlem6  38310  poimirlem7  38311  poimirlem8  38312  poimirlem15  38319  poimirlem20  38324  poimirlem28  38332  opnmbllem0  38340  itg2gt0cn  38359  ftc1cnnclem  38375  ftc1anc  38385  cntotbnd  38480  3lexlogpow5ineq3  42857  3lexlogpow2ineq2  42859  3lexlogpow5ineq5  42860  aks4d1lem1  42862  0nonelalab  42867  aks4d1p1p3  42869  aks4d1p1p2  42870  aks4d1p1p4  42871  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p2  42877  aks4d1p3  42878  aks4d1p6  42881  aks4d1p7d1  42882  aks4d1p7  42883  aks4d1p8d3  42886  aks4d1p8  42887  2ap1caineq  42945  sticksstones1  42946  sn-addlt0d  43265  sn-addgt0d  43266  sn-mulgt1d  43286  fimgmcyc  43335  flt4lem7  43424  fltnlta  43428  pellexlem5  43593  pellfundex  43646  pellfundrp  43648  rmspecfund  43669  monotuz  43701  jm3.1lem2  43778  jm3.1lem3  43779  imo72b2  44931  prmunb2  45054  ltadd12dd  46092  infleinflem2  46119  sqrlearg  46302  lptre2pt  46387  0ellimcdiv  46396  limsup10exlem  46519  ioodvbdlimc1lem1  46678  iblspltprt  46720  itgspltprt  46726  stoweidlem7  46754  stoweidlem11  46758  stoweidlem13  46760  stoweidlem14  46761  stoweidlem26  46773  stoweidlem42  46789  stoweidlem52  46799  stoweidlem59  46806  stoweidlem60  46807  stoweidlem62  46809  wallispilem4  46815  wallispi  46817  stirlinglem1  46821  stirlinglem3  46823  stirlinglem6  46826  stirlinglem7  46827  stirlinglem10  46830  stirlinglem11  46831  dirkercncflem1  46850  dirkercncflem2  46851  fourierdlem10  46864  fourierdlem11  46865  fourierdlem12  46866  fourierdlem42  46896  fourierdlem47  46900  fourierdlem50  46903  fourierdlem51  46904  fourierdlem73  46926  fourierdlem79  46932  fourierdlem83  46936  fourierdlem103  46956  fourierdlem104  46957  sqwvfoura  46975  sqwvfourb  46976  fouriersw  46978  hoidmvlelem1  47342  hoiqssbllem2  47370  hspmbllem1  47373  pimrecltpos  47455  pimrecltneg  47471  smfaddlem1  47510  smflimlem3  47520  smflimlem4  47521  smfmullem1  47538  ormkglobd  47624  chnsubseq  47629  difmodm1lt  48135  2timesltsqm1  48149  fpprel2  48539  gpgedgvtx0  48859  gpgedgvtx1  48860  eenglngeehlnmlem2  49551