Theorem lttrd 11394

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   < clt 11267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is referenced by:  mulgt1  12101  nnne0  12272  expgt1  14116  ltexp2a  14182  expcan  14185  ltexp2  14186  leexp2  14187  expnlbnd2  14250  expmulnbnd  14251  reccn2  15611  efgt1  16132  tanhlt1  16176  ruclem2  16248  isprm7  16725  pythagtriplem13  16845  fldivp1  16915  4sqlem12  16974  sylow1lem1  19577  telgsums  19972  chfacffsupp  22792  chfacfscmul0  22794  chfacfpmmul0  22798  nrginvrcnlem  24628  iccntr  24759  icccmplem2  24761  opnreen  24769  pjthlem1  25387  pmltpclem2  25400  ovollb2lem  25439  opnmbllem  25552  volivth  25558  lhop1lem  25968  dvcnvrelem1  25972  dvcvx  25975  ftc1lem4  25996  aaliou3lem7  26307  ulmdvlem1  26359  reeff1olem  26406  pilem2  26412  pilem3  26413  tangtx  26464  tanord1  26496  tanord  26497  rplogcl  26563  logimul  26573  logcnlem3  26603  efopnlem1  26615  cxplt  26653  cxple  26654  cxpcn3lem  26707  asinsin  26852  atanlogaddlem  26873  atanlogsublem  26875  cxp2limlem  26936  cxp2lim  26937  zetacvg  26975  lgamucov  26998  lgamcvg2  27015  ftalem1  27033  mersenne  27188  bposlem2  27246  bposlem6  27250  bposlem9  27253  lgsqrlem2  27308  lgsquadlem2  27342  chebbnd1lem2  27431  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  chto1ub  27437  mulog2sumlem2  27496  chpdifbndlem1  27514  selberg3lem1  27518  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem1  27550  pntibndlem2  27552  pntibndlem3  27553  pntibnd  27554  pntlemb  27558  pntlemr  27563  pntlemf  27566  pnt  27575  ostth2lem1  27579  ostth2lem3  27596  ostth2lem4  27597  wwlksext2clwwlk  29984  frgrogt3nreg  30324  friendshipgt3  30325  pjhthlem1  31318  sgnsub  32762  chnub  32938  psgnfzto1stlem  33057  1smat1  33781  sqsscirc1  33885  xrge0iifiso  33912  signslema  34540  chtvalz  34607  hgt750lemd  34626  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem20  36495  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem15  37605  poimirlem20  37610  poimirlem28  37618  opnmbllem0  37626  itg2gt0cn  37645  ftc1cnnclem  37661  ftc1anc  37671  cntotbnd  37766  3lexlogpow5ineq3  42016  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  0nonelalab  42026  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8d3  42045  aks4d1p8  42046  2ap1caineq  42104  sticksstones1  42105  sn-addlt0d  42436  sn-addgt0d  42437  sn-mulgt1d  42455  fimgmcyc  42504  flt4lem7  42629  fltnlta  42633  pellexlem5  42803  pellfundex  42856  pellfundrp  42858  rmspecfund  42879  monotuz  42912  jm3.1lem2  42989  jm3.1lem3  42990  imo72b2  44143  prmunb2  44283  neglt  45261  ltadd12dd  45318  infleinflem2  45346  sqrlearg  45530  lptre2pt  45617  0ellimcdiv  45626  limsup10exlem  45749  ioodvbdlimc1lem1  45908  iblspltprt  45950  itgspltprt  45956  stoweidlem7  45984  stoweidlem11  45988  stoweidlem13  45990  stoweidlem14  45991  stoweidlem26  46003  stoweidlem42  46019  stoweidlem52  46029  stoweidlem59  46036  stoweidlem60  46037  stoweidlem62  46039  wallispilem4  46045  wallispi  46047  stirlinglem1  46051  stirlinglem3  46053  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  dirkercncflem1  46080  dirkercncflem2  46081  fourierdlem10  46094  fourierdlem11  46095  fourierdlem12  46096  fourierdlem42  46126  fourierdlem47  46130  fourierdlem50  46133  fourierdlem51  46134  fourierdlem73  46156  fourierdlem79  46162  fourierdlem83  46166  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  hoidmvlelem1  46572  hoiqssbllem2  46600  hspmbllem1  46603  pimrecltpos  46685  pimrecltneg  46701  smfaddlem1  46740  smflimlem3  46750  smflimlem4  46751  smfmullem1  46768  ormkglobd  46852  fpprel2  47703  gpgedgvtx0  48013  gpgedgvtx1  48014  eenglngeehlnmlem2  48666