Theorem lttrd 11464

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 11379	. . 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 2145   class class class wbr 5103  ℝcr 11192   < clt 11336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341

This theorem is used by:  mulgt1  12171  nnne0  12365  neglt  13133  expgt1  14236  ltexp2a  14302  expcan  14305  ltexp2  14306  leexp2  14307  expnlbnd2  14371  expmulnbnd  14372  sgnsub  15252  reccn2  15757  efgt1  16277  tanhlt1  16321  ruclem2  16393  isprm7  16877  pythagtriplem13  16998  fldivp1  17068  4sqlem12  17127  chnub  18789  chnccat  18793  sylow1lem1  19805  telgsums  20200  chfacffsupp  23167  chfacfscmul0  23169  chfacfpmmul0  23173  nrginvrcnlem  25003  iccntr  25134  icccmplem2  25136  opnreen  25144  pjthlem1  25751  pmltpclem2  25763  ovollb2lem  25802  opnmbllem  25915  volivth  25921  lhop1lem  26326  dvcnvrelem1  26330  dvcvx  26333  ftc1lem4  26352  aaliou3lem7  26669  ulmdvlem1  26720  reeff1olem  26766  pilem2  26772  pilem3  26773  tangtx  26827  tanord1  26858  tanord  26859  rplogcl  26925  logimul  26935  logcnlem3  26965  efopnlem1  26977  cxplt  27015  cxple  27016  cxpcn3lem  27068  asinsin  27213  atanlogaddlem  27234  atanlogsublem  27236  cxp2limlem  27296  cxp2lim  27297  zetacvg  27335  lgamucov  27358  lgamcvg2  27375  ftalem1  27393  mersenne  27547  bposlem2  27605  bposlem6  27609  bposlem9  27612  lgsqrlem2  27667  lgsquadlem2  27701  chebbnd1lem2  27790  chebbnd1lem3  27791  chebbnd1  27792  chtppilimlem1  27793  chto1ub  27796  mulog2sumlem2  27855  chpdifbndlem1  27873  selberg3lem1  27877  pntrlog2bndlem2  27898  pntrlog2bndlem4  27900  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntibndlem1  27909  pntibndlem2  27911  pntibndlem3  27912  pntibnd  27913  pntlemb  27917  pntlemr  27922  pntlemf  27925  pnt  27934  ostth2lem1  27938  ostth2lem3  27955  ostth2lem4  27956  flt4lem7  27982  wwlksext2clwwlk  30641  frgrogt3nreg  30991  friendshipgt3  30992  pjhthlem1  31986  psgnfzto1stlem  33654  1smat1  34429  sqsscirc1  34533  xrge0iifiso  34560  signslema  35184  chtvalz  35251  hgt750lemd  35270  knoppndvlem12  37369  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem17  37374  knoppndvlem20  37377  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem15  38533  poimirlem20  38538  poimirlem28  38546  opnmbllem0  38554  itg2gt0cn  38573  ftc1cnnclem  38589  ftc1anc  38599  cntotbnd  38710  3lexlogpow5ineq3  43087  3lexlogpow2ineq2  43089  3lexlogpow5ineq5  43090  aks4d1lem1  43092  0nonelalab  43097  aks4d1p1p3  43099  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p2  43107  aks4d1p3  43108  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8d3  43116  aks4d1p8  43117  2ap1caineq  43175  sticksstones1  43176  sn-addlt0d  43502  sn-addgt0d  43503  sn-mulgt1d  43523  fimgmcyc  43578  fltnlta  43654  pellexlem5  43819  pellfundex  43872  pellfundrp  43874  rmspecfund  43895  monotuz  43927  jm3.1lem2  44004  jm3.1lem3  44005  imo72b2  45157  prmunb2  45280  ltadd12dd  46324  infleinflem2  46351  sqrlearg  46534  lptre2pt  46619  0ellimcdiv  46628  limsup10exlem  46751  ioodvbdlimc1lem1  46910  iblspltprt  46952  itgspltprt  46958  stoweidlem7  46986  stoweidlem11  46990  stoweidlem13  46992  stoweidlem14  46993  stoweidlem26  47005  stoweidlem42  47021  stoweidlem52  47031  stoweidlem59  47038  stoweidlem60  47039  stoweidlem62  47041  wallispilem4  47047  wallispi  47049  stirlinglem1  47053  stirlinglem3  47055  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem11  47063  dirkercncflem1  47082  dirkercncflem2  47083  fourierdlem10  47096  fourierdlem11  47097  fourierdlem12  47098  fourierdlem42  47128  fourierdlem47  47132  fourierdlem50  47135  fourierdlem51  47136  fourierdlem73  47158  fourierdlem79  47164  fourierdlem83  47168  fourierdlem103  47188  fourierdlem104  47189  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  hoidmvlelem1  47574  hoiqssbllem2  47602  hspmbllem1  47605  pimrecltpos  47687  pimrecltneg  47703  smfaddlem1  47742  smflimlem3  47752  smflimlem4  47753  smfmullem1  47770  ormkglobd  47856  chnsubseq  47859  difmodm1lt  48404  2timesltsqm1  48418  fpprel2  48808  gpgedgvtx0  49128  gpgedgvtx1  49129  eenglngeehlnmlem2  49819