Theorem lttrd 11472

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 11387	. . 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 2144   class class class wbr 5102  ℝcr 11200   < clt 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11258  ax-pre-lttrn 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-ltxr 11349

This theorem is used by:  mulgt1  12179  nnne0  12373  neglt  13141  expgt1  14244  ltexp2a  14310  expcan  14313  ltexp2  14314  leexp2  14315  expnlbnd2  14379  expmulnbnd  14380  sgnsub  15260  reccn2  15765  efgt1  16285  tanhlt1  16329  ruclem2  16401  isprm7  16885  pythagtriplem13  17006  fldivp1  17076  4sqlem12  17135  chnub  18797  chnccat  18801  sylow1lem1  19813  telgsums  20208  chfacffsupp  23175  chfacfscmul0  23177  chfacfpmmul0  23181  nrginvrcnlem  25011  iccntr  25142  icccmplem2  25144  opnreen  25152  pjthlem1  25759  pmltpclem2  25771  ovollb2lem  25810  opnmbllem  25923  volivth  25929  lhop1lem  26334  dvcnvrelem1  26338  dvcvx  26341  ftc1lem4  26360  aaliou3lem7  26677  ulmdvlem1  26728  reeff1olem  26774  pilem2  26780  pilem3  26781  tangtx  26835  tanord1  26866  tanord  26867  rplogcl  26933  logimul  26943  logcnlem3  26973  efopnlem1  26985  cxplt  27023  cxple  27024  cxpcn3lem  27076  asinsin  27221  atanlogaddlem  27242  atanlogsublem  27244  cxp2limlem  27304  cxp2lim  27305  zetacvg  27343  lgamucov  27366  lgamcvg2  27383  ftalem1  27401  mersenne  27555  bposlem2  27613  bposlem6  27617  bposlem9  27620  lgsqrlem2  27675  lgsquadlem2  27709  chebbnd1lem2  27798  chebbnd1lem3  27799  chebbnd1  27800  chtppilimlem1  27801  chto1ub  27804  mulog2sumlem2  27863  chpdifbndlem1  27881  selberg3lem1  27885  pntrlog2bndlem2  27906  pntrlog2bndlem4  27908  pntpbnd1a  27913  pntpbnd1  27914  pntpbnd2  27915  pntibndlem1  27917  pntibndlem2  27919  pntibndlem3  27920  pntibnd  27921  pntlemb  27925  pntlemr  27930  pntlemf  27933  pnt  27942  ostth2lem1  27946  ostth2lem3  27963  ostth2lem4  27964  flt4lem7  27990  wwlksext2clwwlk  30649  frgrogt3nreg  30999  friendshipgt3  31000  pjhthlem1  31994  psgnfzto1stlem  33704  1smat1  34479  sqsscirc1  34583  xrge0iifiso  34610  signslema  35234  chtvalz  35301  hgt750lemd  35320  knoppndvlem12  37432  knoppndvlem14  37434  knoppndvlem15  37435  knoppndvlem17  37437  knoppndvlem20  37440  poimirlem6  38588  poimirlem7  38589  poimirlem8  38590  poimirlem15  38597  poimirlem20  38602  poimirlem28  38610  opnmbllem0  38618  itg2gt0cn  38637  ftc1cnnclem  38653  ftc1anc  38663  cntotbnd  38774  3lexlogpow5ineq3  43151  3lexlogpow2ineq2  43153  3lexlogpow5ineq5  43154  aks4d1lem1  43156  0nonelalab  43161  aks4d1p1p3  43163  aks4d1p1p2  43164  aks4d1p1p4  43165  aks4d1p1p6  43167  aks4d1p1p7  43168  aks4d1p1p5  43169  aks4d1p1  43170  aks4d1p2  43171  aks4d1p3  43172  aks4d1p6  43175  aks4d1p7d1  43176  aks4d1p7  43177  aks4d1p8d3  43180  aks4d1p8  43181  2ap1caineq  43239  sticksstones1  43240  sn-addlt0d  43566  sn-addgt0d  43567  sn-mulgt1d  43587  fimgmcyc  43642  fltnlta  43718  pellexlem5  43884  pellfundex  43937  pellfundrp  43939  rmspecfund  43960  monotuz  43992  jm3.1lem2  44069  jm3.1lem3  44070  imo72b2  45216  prmunb2  45339  ltadd12dd  46399  infleinflem2  46426  sqrlearg  46609  lptre2pt  46694  0ellimcdiv  46703  limsup10exlem  46826  ioodvbdlimc1lem1  46985  iblspltprt  47027  itgspltprt  47033  stoweidlem7  47061  stoweidlem11  47065  stoweidlem13  47067  stoweidlem14  47068  stoweidlem26  47080  stoweidlem42  47096  stoweidlem52  47106  stoweidlem59  47113  stoweidlem60  47114  stoweidlem62  47116  wallispilem4  47122  wallispi  47124  stirlinglem1  47128  stirlinglem3  47130  stirlinglem6  47133  stirlinglem7  47134  stirlinglem10  47137  stirlinglem11  47138  dirkercncflem1  47157  dirkercncflem2  47158  fourierdlem10  47171  fourierdlem11  47172  fourierdlem12  47173  fourierdlem42  47203  fourierdlem47  47207  fourierdlem50  47210  fourierdlem51  47211  fourierdlem73  47233  fourierdlem79  47239  fourierdlem83  47243  fourierdlem103  47263  fourierdlem104  47264  sqwvfoura  47282  sqwvfourb  47283  fouriersw  47285  hoidmvlelem1  47649  hoiqssbllem2  47677  hspmbllem1  47680  pimrecltpos  47762  pimrecltneg  47778  smfaddlem1  47817  smflimlem3  47827  smflimlem4  47828  smfmullem1  47845  ormkglobd  47931  chnsubseq  47934  difmodm1lt  48479  2timesltsqm1  48493  fpprel2  48883  gpgedgvtx0  49203  gpgedgvtx1  49204  eenglngeehlnmlem2  49894