Theorem lttrd 11412

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   class class class wbr 5149  ℝcr 11144   < clt 11285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11202  ax-pre-lttrn 11220

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11287  df-mnf 11288  df-ltxr 11290

This theorem is referenced by:  nnne0  12284  expgt1  14106  ltexp2a  14171  expcan  14174  ltexp2  14175  leexp2  14176  expnlbnd2  14237  expmulnbnd  14238  reccn2  15585  efgt1  16104  tanhlt1  16148  ruclem2  16220  isprm7  16695  pythagtriplem13  16815  fldivp1  16885  4sqlem12  16944  sylow1lem1  19582  telgsums  19977  chfacffsupp  22819  chfacfscmul0  22821  chfacfpmmul0  22825  nrginvrcnlem  24669  iccntr  24798  icccmplem2  24800  opnreen  24808  pjthlem1  25426  pmltpclem2  25439  ovollb2lem  25478  opnmbllem  25591  volivth  25597  lhop1lem  26007  dvcnvrelem1  26011  dvcvx  26014  ftc1lem4  26035  aaliou3lem7  26346  ulmdvlem1  26398  reeff1olem  26445  pilem2  26451  pilem3  26452  tangtx  26502  tanord1  26533  tanord  26534  rplogcl  26600  logimul  26610  logcnlem3  26640  efopnlem1  26652  cxplt  26690  cxple  26691  cxpcn3lem  26744  asinsin  26889  atanlogaddlem  26910  atanlogsublem  26912  cxp2limlem  26973  cxp2lim  26974  zetacvg  27012  lgamucov  27035  lgamcvg2  27052  ftalem1  27070  mersenne  27225  bposlem2  27283  bposlem6  27287  bposlem9  27290  lgsqrlem2  27345  lgsquadlem2  27379  chebbnd1lem2  27468  chebbnd1lem3  27469  chebbnd1  27470  chtppilimlem1  27471  chto1ub  27474  mulog2sumlem2  27533  chpdifbndlem1  27551  selberg3lem1  27555  pntrlog2bndlem2  27576  pntrlog2bndlem4  27578  pntpbnd1a  27583  pntpbnd1  27584  pntpbnd2  27585  pntibndlem1  27587  pntibndlem2  27589  pntibndlem3  27590  pntibnd  27591  pntlemb  27595  pntlemr  27600  pntlemf  27603  pnt  27612  ostth2lem1  27616  ostth2lem3  27633  ostth2lem4  27634  wwlksext2clwwlk  29959  frgrogt3nreg  30299  friendshipgt3  30300  pjhthlem1  31293  psgnfzto1stlem  32934  1smat1  33556  sqsscirc1  33660  xrge0iifiso  33687  sgnsub  34315  signslema  34345  chtvalz  34412  hgt750lemd  34431  knoppndvlem12  36149  knoppndvlem14  36151  knoppndvlem15  36152  knoppndvlem17  36154  knoppndvlem20  36157  poimirlem6  37250  poimirlem7  37251  poimirlem8  37252  poimirlem15  37259  poimirlem20  37264  poimirlem28  37272  opnmbllem0  37280  itg2gt0cn  37299  ftc1cnnclem  37315  ftc1anc  37325  cntotbnd  37420  3lexlogpow5ineq3  41680  3lexlogpow2ineq2  41682  3lexlogpow5ineq5  41683  aks4d1lem1  41685  0nonelalab  41690  aks4d1p1p3  41692  aks4d1p1p2  41693  aks4d1p1p4  41694  aks4d1p1p6  41696  aks4d1p1p7  41697  aks4d1p1p5  41698  aks4d1p1  41699  aks4d1p2  41700  aks4d1p3  41701  aks4d1p6  41704  aks4d1p7d1  41705  aks4d1p7  41706  aks4d1p8d3  41709  aks4d1p8  41710  2ap1caineq  41767  sticksstones1  41768  sn-addlt0d  42141  sn-addgt0d  42142  flt4lem7  42223  fltnlta  42227  pellexlem5  42400  pellfundex  42453  pellfundrp  42455  rmspecfund  42476  monotuz  42509  jm3.1lem2  42586  jm3.1lem3  42587  imo72b2  43749  prmunb2  43895  neglt  44809  ltadd12dd  44868  infleinflem2  44896  sqrlearg  45081  lptre2pt  45171  0ellimcdiv  45180  limsup10exlem  45303  ioodvbdlimc1lem1  45462  iblspltprt  45504  itgspltprt  45510  stoweidlem7  45538  stoweidlem11  45542  stoweidlem13  45544  stoweidlem14  45545  stoweidlem26  45557  stoweidlem42  45573  stoweidlem52  45583  stoweidlem59  45590  stoweidlem60  45591  stoweidlem62  45593  wallispilem4  45599  wallispi  45601  stirlinglem1  45605  stirlinglem3  45607  stirlinglem6  45610  stirlinglem7  45611  stirlinglem10  45614  stirlinglem11  45615  dirkercncflem1  45634  dirkercncflem2  45635  fourierdlem10  45648  fourierdlem11  45649  fourierdlem12  45650  fourierdlem42  45680  fourierdlem47  45684  fourierdlem50  45687  fourierdlem51  45688  fourierdlem73  45710  fourierdlem79  45716  fourierdlem83  45720  fourierdlem103  45740  fourierdlem104  45741  sqwvfoura  45759  sqwvfourb  45760  fouriersw  45762  hoidmvlelem1  46126  hoiqssbllem2  46154  hspmbllem1  46157  pimrecltpos  46239  pimrecltneg  46255  smfaddlem1  46294  smflimlem3  46304  smflimlem4  46305  smfmullem1  46322  fpprel2  47223  eenglngeehlnmlem2  48002