Theorem lttrd 10958

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112   class class class wbr 5039  ℝcr 10693   < clt 10832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-pre-lttrn 10769

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837

This theorem is referenced by:  nnne0  11829  expgt1  13638  ltexp2a  13701  expcan  13704  ltexp2  13705  leexp2  13706  expnlbnd2  13766  expmulnbnd  13767  reccn2  15123  efgt1  15640  tanhlt1  15684  ruclem2  15756  isprm7  16228  pythagtriplem13  16343  fldivp1  16413  4sqlem12  16472  sylow1lem1  18941  telgsums  19332  chfacffsupp  21707  chfacfscmul0  21709  chfacfpmmul0  21713  nrginvrcnlem  23543  iccntr  23672  icccmplem2  23674  opnreen  23682  pjthlem1  24288  pmltpclem2  24300  ovollb2lem  24339  opnmbllem  24452  volivth  24458  lhop1lem  24864  dvcnvrelem1  24868  dvcvx  24871  ftc1lem4  24890  aaliou3lem7  25196  ulmdvlem1  25246  reeff1olem  25292  pilem2  25298  pilem3  25299  tangtx  25349  tanord1  25380  tanord  25381  rplogcl  25446  logimul  25456  logcnlem3  25486  efopnlem1  25498  cxplt  25536  cxple  25537  cxpcn3lem  25587  asinsin  25729  atanlogaddlem  25750  atanlogsublem  25752  cxp2limlem  25812  cxp2lim  25813  zetacvg  25851  lgamucov  25874  lgamcvg2  25891  ftalem1  25909  mersenne  26062  bposlem2  26120  bposlem6  26124  bposlem9  26127  lgsqrlem2  26182  lgsquadlem2  26216  chebbnd1lem2  26305  chebbnd1lem3  26306  chebbnd1  26307  chtppilimlem1  26308  chto1ub  26311  mulog2sumlem2  26370  chpdifbndlem1  26388  selberg3lem1  26392  pntrlog2bndlem2  26413  pntrlog2bndlem4  26415  pntpbnd1a  26420  pntpbnd1  26421  pntpbnd2  26422  pntibndlem1  26424  pntibndlem2  26426  pntibndlem3  26427  pntibnd  26428  pntlemb  26432  pntlemr  26437  pntlemf  26440  pnt  26449  ostth2lem1  26453  ostth2lem3  26470  ostth2lem4  26471  wwlksext2clwwlk  28094  frgrogt3nreg  28434  friendshipgt3  28435  pjhthlem1  29426  psgnfzto1stlem  31040  1smat1  31422  sqsscirc1  31526  xrge0iifiso  31553  sgnsub  32177  signslema  32207  chtvalz  32275  hgt750lemd  32294  knoppndvlem12  34389  knoppndvlem14  34391  knoppndvlem15  34392  knoppndvlem17  34394  knoppndvlem20  34397  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem15  35478  poimirlem20  35483  poimirlem28  35491  opnmbllem0  35499  itg2gt0cn  35518  ftc1cnnclem  35534  ftc1anc  35544  cntotbnd  35640  3lexlogpow5ineq3  39748  3lexlogpow2ineq2  39750  3lexlogpow5ineq5  39751  0nonelalab  39757  aks4d1p1p3  39759  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1p6  39763  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  2ap1caineq  39770  sticksstones1  39771  flt4lem7  40140  fltnlta  40144  pellexlem5  40299  pellfundex  40352  pellfundrp  40354  rmspecfund  40375  monotuz  40407  jm3.1lem2  40484  jm3.1lem3  40485  imo72b2  41402  prmunb2  41543  neglt  42436  ltadd12dd  42496  infleinflem2  42524  sqrlearg  42707  lptre2pt  42799  0ellimcdiv  42808  limsup10exlem  42931  ioodvbdlimc1lem1  43090  iblspltprt  43132  itgspltprt  43138  stoweidlem7  43166  stoweidlem11  43170  stoweidlem13  43172  stoweidlem14  43173  stoweidlem26  43185  stoweidlem42  43201  stoweidlem52  43211  stoweidlem59  43218  stoweidlem60  43219  stoweidlem62  43221  wallispilem4  43227  wallispi  43229  stirlinglem1  43233  stirlinglem3  43235  stirlinglem6  43238  stirlinglem7  43239  stirlinglem10  43242  stirlinglem11  43243  dirkercncflem1  43262  dirkercncflem2  43263  fourierdlem10  43276  fourierdlem11  43277  fourierdlem12  43278  fourierdlem42  43308  fourierdlem47  43312  fourierdlem50  43315  fourierdlem51  43316  fourierdlem73  43338  fourierdlem79  43344  fourierdlem83  43348  fourierdlem103  43368  fourierdlem104  43369  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  hoidmvlelem1  43751  hoiqssbllem2  43779  hspmbllem1  43782  pimrecltpos  43861  pimrecltneg  43875  smfaddlem1  43913  smflimlem3  43923  smflimlem4  43924  smfmullem1  43940  fpprel2  44809  eenglngeehlnmlem2  45700