Theorem lttrd 10452

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2155   class class class wbr 4809  ℝcr 10188   < clt 10328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-resscn 10246  ax-pre-lttrn 10264

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-ltxr 10333

This theorem is referenced by:  expgt1  13105  ltexp2a  13119  expcan  13120  ltexp2  13121  leexp2  13122  expnlbnd2  13202  expmulnbnd  13203  reccn2  14612  efgt1  15128  tanhlt1  15172  ruclem2  15243  isprm7  15699  pythagtriplem13  15811  fldivp1  15880  4sqlem12  15939  sylow1lem1  18277  telgsums  18657  chfacffsupp  20940  chfacfscmul0  20942  chfacfpmmul0  20946  nrginvrcnlem  22774  iccntr  22903  icccmplem2  22905  opnreen  22913  pjthlem1  23497  pmltpclem2  23507  ovollb2lem  23546  opnmbllem  23659  volivth  23665  lhop1lem  24067  dvcnvrelem1  24071  dvcvx  24074  ftc1lem4  24093  aaliou3lem7  24395  ulmdvlem1  24445  reeff1olem  24491  pilem2  24497  pilem3  24498  pilem3OLD  24499  tangtx  24549  tanord1  24575  tanord  24576  rplogcl  24641  logimul  24651  logcnlem3  24681  efopnlem1  24693  cxplt  24731  cxple  24732  cxpcn3lem  24779  asinsin  24910  atanlogaddlem  24931  atanlogsublem  24933  cxp2limlem  24993  cxp2lim  24994  zetacvg  25032  lgamucov  25055  lgamcvg2  25072  ftalem1  25090  mersenne  25243  bposlem2  25301  bposlem6  25305  bposlem9  25308  lgsqrlem2  25363  lgsquadlem2  25397  chebbnd1lem2  25450  chebbnd1lem3  25451  chebbnd1  25452  chtppilimlem1  25453  chto1ub  25456  mulog2sumlem2  25515  chpdifbndlem1  25533  selberg3lem1  25537  pntrlog2bndlem2  25558  pntrlog2bndlem4  25560  pntpbnd1a  25565  pntpbnd1  25566  pntpbnd2  25567  pntibndlem1  25569  pntibndlem2  25571  pntibndlem3  25572  pntibnd  25573  pntlemb  25577  pntlemr  25582  pntlemf  25585  pnt  25594  ostth2lem1  25598  ostth2lem3  25615  ostth2lem4  25616  wwlksext2clwwlk  27307  wwlksext2clwwlkOLD  27308  frgrogt3nreg  27713  friendshipgt3  27714  pjhthlem1  28706  psgnfzto1stlem  30297  1smat1  30317  sqsscirc1  30401  xrge0iifiso  30428  sgnsub  31054  signslema  31088  chtvalz  31158  hgt750lemd  31177  knoppndvlem12  32953  knoppndvlem14  32955  knoppndvlem15  32956  knoppndvlem17  32958  knoppndvlem20  32961  poimirlem6  33839  poimirlem7  33840  poimirlem8  33841  poimirlem15  33848  poimirlem20  33853  poimirlem28  33861  opnmbllem0  33869  itg2gt0cn  33888  ftc1cnnclem  33906  ftc1anc  33916  cntotbnd  34017  pellexlem5  38075  pellfundex  38128  pellfundrp  38130  rmspecfund  38151  monotuz  38183  jm3.1lem2  38262  jm3.1lem3  38263  imo72b2  39149  prmunb2  39184  neglt  40136  ltadd12dd  40197  infleinflem2  40225  sqrlearg  40418  lptre2pt  40510  0ellimcdiv  40519  limsup10exlem  40642  ioodvbdlimc1lem1  40784  iblspltprt  40826  itgspltprt  40832  stoweidlem7  40861  stoweidlem11  40865  stoweidlem13  40867  stoweidlem14  40868  stoweidlem26  40880  stoweidlem42  40896  stoweidlem52  40906  stoweidlem59  40913  stoweidlem60  40914  stoweidlem62  40916  wallispilem4  40922  wallispi  40924  stirlinglem1  40928  stirlinglem3  40930  stirlinglem6  40933  stirlinglem7  40934  stirlinglem10  40937  stirlinglem11  40938  dirkercncflem1  40957  dirkercncflem2  40958  fourierdlem10  40971  fourierdlem11  40972  fourierdlem12  40973  fourierdlem42  41003  fourierdlem47  41007  fourierdlem50  41010  fourierdlem51  41011  fourierdlem73  41033  fourierdlem79  41039  fourierdlem83  41043  fourierdlem103  41063  fourierdlem104  41064  sqwvfoura  41082  sqwvfourb  41083  fouriersw  41085  hoidmvlelem1  41449  hoiqssbllem2  41477  hspmbllem1  41480  pimrecltpos  41559  pimrecltneg  41573  smfaddlem1  41611  smflimlem3  41621  smflimlem4  41622  smfmullem1  41638