Theorem lttrd 11294

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttrn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171

This theorem is referenced by:  mulgt1  12003  nnne0  12179  neglt  12925  expgt1  14023  ltexp2a  14089  expcan  14092  ltexp2  14093  leexp2  14094  expnlbnd2  14157  expmulnbnd  14158  reccn2  15520  efgt1  16041  tanhlt1  16085  ruclem2  16157  isprm7  16635  pythagtriplem13  16755  fldivp1  16825  4sqlem12  16884  chnub  18545  chnccat  18549  sylow1lem1  19527  telgsums  19922  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  nrginvrcnlem  24635  iccntr  24766  icccmplem2  24768  opnreen  24776  pjthlem1  25393  pmltpclem2  25406  ovollb2lem  25445  opnmbllem  25558  volivth  25564  lhop1lem  25974  dvcnvrelem1  25978  dvcvx  25981  ftc1lem4  26002  aaliou3lem7  26313  ulmdvlem1  26365  reeff1olem  26412  pilem2  26418  pilem3  26419  tangtx  26470  tanord1  26502  tanord  26503  rplogcl  26569  logimul  26579  logcnlem3  26609  efopnlem1  26621  cxplt  26659  cxple  26660  cxpcn3lem  26713  asinsin  26858  atanlogaddlem  26879  atanlogsublem  26881  cxp2limlem  26942  cxp2lim  26943  zetacvg  26981  lgamucov  27004  lgamcvg2  27021  ftalem1  27039  mersenne  27194  bposlem2  27252  bposlem6  27256  bposlem9  27259  lgsqrlem2  27314  lgsquadlem2  27348  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chto1ub  27443  mulog2sumlem2  27502  chpdifbndlem1  27520  selberg3lem1  27524  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem1  27556  pntibndlem2  27558  pntibndlem3  27559  pntibnd  27560  pntlemb  27564  pntlemr  27569  pntlemf  27572  pnt  27581  ostth2lem1  27585  ostth2lem3  27602  ostth2lem4  27603  wwlksext2clwwlk  30132  frgrogt3nreg  30472  friendshipgt3  30473  pjhthlem1  31466  sgnsub  32918  psgnfzto1stlem  33182  1smat1  33961  sqsscirc1  34065  xrge0iifiso  34092  signslema  34719  chtvalz  34786  hgt750lemd  34805  knoppndvlem12  36723  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem20  36731  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem15  37836  poimirlem20  37841  poimirlem28  37849  opnmbllem0  37857  itg2gt0cn  37876  ftc1cnnclem  37892  ftc1anc  37902  cntotbnd  37997  3lexlogpow5ineq3  42311  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1lem1  42316  0nonelalab  42321  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8d3  42340  aks4d1p8  42341  2ap1caineq  42399  sticksstones1  42400  sn-addlt0d  42713  sn-addgt0d  42714  sn-mulgt1d  42734  fimgmcyc  42789  flt4lem7  42902  fltnlta  42906  pellexlem5  43075  pellfundex  43128  pellfundrp  43130  rmspecfund  43151  monotuz  43183  jm3.1lem2  43260  jm3.1lem3  43261  imo72b2  44413  prmunb2  44552  ltadd12dd  45588  infleinflem2  45615  sqrlearg  45799  lptre2pt  45884  0ellimcdiv  45893  limsup10exlem  46016  ioodvbdlimc1lem1  46175  iblspltprt  46217  itgspltprt  46223  stoweidlem7  46251  stoweidlem11  46255  stoweidlem13  46257  stoweidlem14  46258  stoweidlem26  46270  stoweidlem42  46286  stoweidlem52  46296  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  wallispilem4  46312  wallispi  46314  stirlinglem1  46318  stirlinglem3  46320  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem11  46328  dirkercncflem1  46347  dirkercncflem2  46348  fourierdlem10  46361  fourierdlem11  46362  fourierdlem12  46363  fourierdlem42  46393  fourierdlem47  46397  fourierdlem50  46400  fourierdlem51  46401  fourierdlem73  46423  fourierdlem79  46429  fourierdlem83  46433  fourierdlem103  46453  fourierdlem104  46454  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  hoidmvlelem1  46839  hoiqssbllem2  46867  hspmbllem1  46870  pimrecltpos  46952  pimrecltneg  46968  smfaddlem1  47007  smflimlem3  47017  smflimlem4  47018  smfmullem1  47035  ormkglobd  47119  chnsubseq  47124  difmodm1lt  47605  fpprel2  47987  gpgedgvtx0  48307  gpgedgvtx1  48308  eenglngeehlnmlem2  48984