Theorem lttrd 10077

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958

This theorem is referenced by:  expgt1  12760  ltexp2a  12774  expcan  12775  ltexp2  12776  leexp2  12777  expnlbnd2  12857  expmulnbnd  12858  reccn2  14175  efgt1  14685  tanhlt1  14729  ruclem2  14800  isprm7  15258  pythagtriplem13  15370  fldivp1  15439  4sqlem12  15498  sylow1lem1  17836  telgsums  18213  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  nrginvrcnlem  22305  iccntr  22432  icccmplem2  22434  opnreen  22442  pjthlem1  23016  pmltpclem2  23025  ovollb2lem  23063  opnmbllem  23175  volivth  23181  lhop1lem  23580  dvcnvrelem1  23584  dvcvx  23587  ftc1lem4  23606  aaliou3lem7  23908  ulmdvlem1  23958  reeff1olem  24004  pilem2  24010  pilem3  24011  tangtx  24061  tanord1  24087  tanord  24088  rplogcl  24154  logimul  24164  logcnlem3  24190  efopnlem1  24202  cxplt  24240  cxple  24241  cxpcn3lem  24288  asinsin  24419  atanlogaddlem  24440  atanlogsublem  24442  cxp2limlem  24502  cxp2lim  24503  zetacvg  24541  lgamucov  24564  lgamcvg2  24581  ftalem1  24599  mersenne  24752  bposlem2  24810  bposlem6  24814  bposlem9  24817  lgsqrlem2  24872  lgsquadlem2  24906  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chto1ub  24965  mulog2sumlem2  25024  chpdifbndlem1  25042  selberg3lem1  25046  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem1  25078  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemb  25086  pntlemr  25091  pntlemf  25094  pnt  25103  ostth2lem1  25107  ostth2lem3  25124  ostth2lem4  25125  wwlkext2clwwlk  26331  eupap1  26503  frgraogt3nreg  26647  friendshipgt3  26648  pjhthlem1  27634  psgnfzto1stlem  29181  1smat1  29198  sqsscirc1  29282  xrge0iifiso  29309  sgnsub  29933  signslema  29965  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem20  31692  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem15  32594  poimirlem20  32599  poimirlem28  32607  opnmbllem0  32615  itg2gt0cn  32635  ftc1cnnclem  32653  ftc1anc  32663  cntotbnd  32765  pellexlem5  36415  pellfundex  36468  pellfundrp  36470  rmspecfund  36492  monotuz  36524  jm3.1lem2  36603  jm3.1lem3  36604  imo72b2  37497  prmunb2  37532  neglt  38437  ltadd12dd  38500  infleinflem2  38528  sqrlearg  38627  lptre2pt  38707  0ellimcdiv  38716  ioodvbdlimc1lem1  38821  iblspltprt  38865  itgspltprt  38871  stoweidlem7  38900  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem26  38919  stoweidlem42  38935  stoweidlem52  38945  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  wallispilem4  38961  wallispi  38963  stirlinglem1  38967  stirlinglem3  38969  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  dirkercncflem1  38996  dirkercncflem2  38997  fourierdlem10  39010  fourierdlem11  39011  fourierdlem12  39012  fourierdlem42  39042  fourierdlem47  39046  fourierdlem50  39049  fourierdlem51  39050  fourierdlem73  39072  fourierdlem79  39078  fourierdlem83  39082  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  hoidmvlelem1  39485  hoiqssbllem2  39513  hspmbllem1  39516  pimrecltpos  39596  pimrecltneg  39610  smfaddlem1  39649  smflimlem3  39659  smflimlem4  39660  smfmullem1  39676  wwlksext2clwwlk  41231  av-frgraogt3nreg  41551  av-friendshipgt3  41552