Theorem lttrd 11338

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   class class class wbr 5097  ℝcr 11066   < clt 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-pre-lttrn 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215

This theorem is referenced by:  mulgt1  12047  nnne0  12241  neglt  13007  expgt1  14107  ltexp2a  14173  expcan  14176  ltexp2  14177  leexp2  14178  expnlbnd2  14241  expmulnbnd  14242  sgnsub  15110  reccn2  15615  efgt1  16139  tanhlt1  16183  ruclem2  16255  isprm7  16734  pythagtriplem13  16854  fldivp1  16924  4sqlem12  16983  chnub  18645  chnccat  18649  sylow1lem1  19629  telgsums  20024  chfacffsupp  22904  chfacfscmul0  22906  chfacfpmmul0  22910  nrginvrcnlem  24739  iccntr  24870  icccmplem2  24872  opnreen  24880  pjthlem1  25487  pmltpclem2  25499  ovollb2lem  25538  opnmbllem  25651  volivth  25657  lhop1lem  26063  dvcnvrelem1  26067  dvcvx  26070  ftc1lem4  26089  aaliou3lem7  26401  ulmdvlem1  26451  reeff1olem  26497  pilem2  26503  pilem3  26504  tangtx  26558  tanord1  26590  tanord  26591  rplogcl  26657  logimul  26667  logcnlem3  26697  efopnlem1  26709  cxplt  26747  cxple  26748  cxpcn3lem  26800  asinsin  26945  atanlogaddlem  26966  atanlogsublem  26968  cxp2limlem  27028  cxp2lim  27029  zetacvg  27067  lgamucov  27090  lgamcvg2  27107  ftalem1  27125  mersenne  27279  bposlem2  27337  bposlem6  27341  bposlem9  27344  lgsqrlem2  27399  lgsquadlem2  27433  chebbnd1lem2  27522  chebbnd1lem3  27523  chebbnd1  27524  chtppilimlem1  27525  chto1ub  27528  mulog2sumlem2  27587  chpdifbndlem1  27605  selberg3lem1  27609  pntrlog2bndlem2  27630  pntrlog2bndlem4  27632  pntpbnd1a  27637  pntpbnd1  27638  pntpbnd2  27639  pntibndlem1  27641  pntibndlem2  27643  pntibndlem3  27644  pntibnd  27645  pntlemb  27649  pntlemr  27654  pntlemf  27657  pnt  27666  ostth2lem1  27670  ostth2lem3  27687  ostth2lem4  27688  wwlksext2clwwlk  30216  frgrogt3nreg  30556  friendshipgt3  30557  pjhthlem1  31551  psgnfzto1stlem  33241  1smat1  34062  sqsscirc1  34166  xrge0iifiso  34193  signslema  34817  chtvalz  34884  hgt750lemd  34903  knoppndvlem12  36922  knoppndvlem14  36924  knoppndvlem15  36925  knoppndvlem17  36927  knoppndvlem20  36930  poimirlem6  38086  poimirlem7  38087  poimirlem8  38088  poimirlem15  38095  poimirlem20  38100  poimirlem28  38108  opnmbllem0  38116  itg2gt0cn  38135  ftc1cnnclem  38151  ftc1anc  38161  cntotbnd  38256  3lexlogpow5ineq3  42635  3lexlogpow2ineq2  42637  3lexlogpow5ineq5  42638  aks4d1lem1  42640  0nonelalab  42645  aks4d1p1p3  42647  aks4d1p1p2  42648  aks4d1p1p4  42649  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  aks4d1p1  42654  aks4d1p2  42655  aks4d1p3  42656  aks4d1p6  42659  aks4d1p7d1  42660  aks4d1p7  42661  aks4d1p8d3  42664  aks4d1p8  42665  2ap1caineq  42723  sticksstones1  42724  sn-addlt0d  43041  sn-addgt0d  43042  sn-mulgt1d  43062  fimgmcyc  43113  flt4lem7  43202  fltnlta  43206  pellexlem5  43371  pellfundex  43424  pellfundrp  43426  rmspecfund  43447  monotuz  43479  jm3.1lem2  43556  jm3.1lem3  43557  imo72b2  44709  prmunb2  44848  ltadd12dd  45880  infleinflem2  45907  sqrlearg  46090  lptre2pt  46175  0ellimcdiv  46184  limsup10exlem  46307  ioodvbdlimc1lem1  46466  iblspltprt  46508  itgspltprt  46514  stoweidlem7  46542  stoweidlem11  46546  stoweidlem13  46548  stoweidlem14  46549  stoweidlem26  46561  stoweidlem42  46577  stoweidlem52  46587  stoweidlem59  46594  stoweidlem60  46595  stoweidlem62  46597  wallispilem4  46603  wallispi  46605  stirlinglem1  46609  stirlinglem3  46611  stirlinglem6  46614  stirlinglem7  46615  stirlinglem10  46618  stirlinglem11  46619  dirkercncflem1  46638  dirkercncflem2  46639  fourierdlem10  46652  fourierdlem11  46653  fourierdlem12  46654  fourierdlem42  46684  fourierdlem47  46688  fourierdlem50  46691  fourierdlem51  46692  fourierdlem73  46714  fourierdlem79  46720  fourierdlem83  46724  fourierdlem103  46744  fourierdlem104  46745  sqwvfoura  46763  sqwvfourb  46764  fouriersw  46766  hoidmvlelem1  47130  hoiqssbllem2  47158  hspmbllem1  47161  pimrecltpos  47243  pimrecltneg  47259  smfaddlem1  47298  smflimlem3  47308  smflimlem4  47309  smfmullem1  47326  ormkglobd  47412  chnsubseq  47417  difmodm1lt  47920  2timesltsqm1  47934  fpprel2  48324  gpgedgvtx0  48644  gpgedgvtx1  48645  eenglngeehlnmlem2  49321