Theorem lttrd 10593

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048   class class class wbr 4923  ℝcr 10326   < clt 10466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-resscn 10384  ax-pre-lttrn 10402

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-er 8081  df-en 8299  df-dom 8300  df-sdom 8301  df-pnf 10468  df-mnf 10469  df-ltxr 10471

This theorem is referenced by:  nnne0  11467  expgt1  13275  ltexp2a  13338  expcan  13341  ltexp2  13342  leexp2  13343  expnlbnd2  13403  expmulnbnd  13404  reccn2  14804  efgt1  15319  tanhlt1  15363  ruclem2  15435  isprm7  15898  pythagtriplem13  16010  fldivp1  16079  4sqlem12  16138  sylow1lem1  18474  telgsums  18853  chfacffsupp  21158  chfacfscmul0  21160  chfacfpmmul0  21164  nrginvrcnlem  22993  iccntr  23122  icccmplem2  23124  opnreen  23132  pjthlem1  23733  pmltpclem2  23743  ovollb2lem  23782  opnmbllem  23895  volivth  23901  lhop1lem  24303  dvcnvrelem1  24307  dvcvx  24310  ftc1lem4  24329  aaliou3lem7  24631  ulmdvlem1  24681  reeff1olem  24727  pilem2  24733  pilem3  24734  tangtx  24784  tanord1  24812  tanord  24813  rplogcl  24878  logimul  24888  logcnlem3  24918  efopnlem1  24930  cxplt  24968  cxple  24969  cxpcn3lem  25019  asinsin  25161  atanlogaddlem  25182  atanlogsublem  25184  cxp2limlem  25245  cxp2lim  25246  zetacvg  25284  lgamucov  25307  lgamcvg2  25324  ftalem1  25342  mersenne  25495  bposlem2  25553  bposlem6  25557  bposlem9  25560  lgsqrlem2  25615  lgsquadlem2  25649  chebbnd1lem2  25738  chebbnd1lem3  25739  chebbnd1  25740  chtppilimlem1  25741  chto1ub  25744  mulog2sumlem2  25803  chpdifbndlem1  25821  selberg3lem1  25825  pntrlog2bndlem2  25846  pntrlog2bndlem4  25848  pntpbnd1a  25853  pntpbnd1  25854  pntpbnd2  25855  pntibndlem1  25857  pntibndlem2  25859  pntibndlem3  25860  pntibnd  25861  pntlemb  25865  pntlemr  25870  pntlemf  25873  pnt  25882  ostth2lem1  25886  ostth2lem3  25903  ostth2lem4  25904  wwlksext2clwwlk  27570  frgrogt3nreg  27944  friendshipgt3  27945  pjhthlem1  28939  psgnfzto1stlem  30648  1smat1  30668  sqsscirc1  30752  xrge0iifiso  30779  sgnsub  31405  signslema  31439  chtvalz  31509  hgt750lemd  31528  knoppndvlem12  33322  knoppndvlem14  33324  knoppndvlem15  33325  knoppndvlem17  33327  knoppndvlem20  33330  poimirlem6  34287  poimirlem7  34288  poimirlem8  34289  poimirlem15  34296  poimirlem20  34301  poimirlem28  34309  opnmbllem0  34317  itg2gt0cn  34336  ftc1cnnclem  34354  ftc1anc  34364  cntotbnd  34464  fltnlta  38627  pellexlem5  38771  pellfundex  38824  pellfundrp  38826  rmspecfund  38847  monotuz  38879  jm3.1lem2  38956  jm3.1lem3  38957  imo72b2  39835  prmunb2  40003  neglt  40925  ltadd12dd  40986  infleinflem2  41014  sqrlearg  41206  lptre2pt  41298  0ellimcdiv  41307  limsup10exlem  41430  ioodvbdlimc1lem1  41592  iblspltprt  41634  itgspltprt  41640  stoweidlem7  41669  stoweidlem11  41673  stoweidlem13  41675  stoweidlem14  41676  stoweidlem26  41688  stoweidlem42  41704  stoweidlem52  41714  stoweidlem59  41721  stoweidlem60  41722  stoweidlem62  41724  wallispilem4  41730  wallispi  41732  stirlinglem1  41736  stirlinglem3  41738  stirlinglem6  41741  stirlinglem7  41742  stirlinglem10  41745  stirlinglem11  41746  dirkercncflem1  41765  dirkercncflem2  41766  fourierdlem10  41779  fourierdlem11  41780  fourierdlem12  41781  fourierdlem42  41811  fourierdlem47  41815  fourierdlem50  41818  fourierdlem51  41819  fourierdlem73  41841  fourierdlem79  41847  fourierdlem83  41851  fourierdlem103  41871  fourierdlem104  41872  sqwvfoura  41890  sqwvfourb  41891  fouriersw  41893  hoidmvlelem1  42254  hoiqssbllem2  42282  hspmbllem1  42285  pimrecltpos  42364  pimrecltneg  42378  smfaddlem1  42416  smflimlem3  42426  smflimlem4  42427  smfmullem1  42443  fpprel2  43214  eenglngeehlnmlem2  44033