Theorem lttrd 11269

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   class class class wbr 5086  ℝcr 11000   < clt 11141

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-pre-lttrn 11076

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-ltxr 11146

This theorem is referenced by:  mulgt1  11978  nnne0  12154  neglt  12905  expgt1  14002  ltexp2a  14068  expcan  14071  ltexp2  14072  leexp2  14073  expnlbnd2  14136  expmulnbnd  14137  reccn2  15499  efgt1  16020  tanhlt1  16064  ruclem2  16136  isprm7  16614  pythagtriplem13  16734  fldivp1  16804  4sqlem12  16863  chnub  18523  chnccat  18527  sylow1lem1  19505  telgsums  19900  chfacffsupp  22766  chfacfscmul0  22768  chfacfpmmul0  22772  nrginvrcnlem  24601  iccntr  24732  icccmplem2  24734  opnreen  24742  pjthlem1  25359  pmltpclem2  25372  ovollb2lem  25411  opnmbllem  25524  volivth  25530  lhop1lem  25940  dvcnvrelem1  25944  dvcvx  25947  ftc1lem4  25968  aaliou3lem7  26279  ulmdvlem1  26331  reeff1olem  26378  pilem2  26384  pilem3  26385  tangtx  26436  tanord1  26468  tanord  26469  rplogcl  26535  logimul  26545  logcnlem3  26575  efopnlem1  26587  cxplt  26625  cxple  26626  cxpcn3lem  26679  asinsin  26824  atanlogaddlem  26845  atanlogsublem  26847  cxp2limlem  26908  cxp2lim  26909  zetacvg  26947  lgamucov  26970  lgamcvg2  26987  ftalem1  27005  mersenne  27160  bposlem2  27218  bposlem6  27222  bposlem9  27225  lgsqrlem2  27280  lgsquadlem2  27314  chebbnd1lem2  27403  chebbnd1lem3  27404  chebbnd1  27405  chtppilimlem1  27406  chto1ub  27409  mulog2sumlem2  27468  chpdifbndlem1  27486  selberg3lem1  27490  pntrlog2bndlem2  27511  pntrlog2bndlem4  27513  pntpbnd1a  27518  pntpbnd1  27519  pntpbnd2  27520  pntibndlem1  27522  pntibndlem2  27524  pntibndlem3  27525  pntibnd  27526  pntlemb  27530  pntlemr  27535  pntlemf  27538  pnt  27547  ostth2lem1  27551  ostth2lem3  27568  ostth2lem4  27569  wwlksext2clwwlk  30029  frgrogt3nreg  30369  friendshipgt3  30370  pjhthlem1  31363  sgnsub  32812  psgnfzto1stlem  33061  1smat1  33809  sqsscirc1  33913  xrge0iifiso  33940  signslema  34567  chtvalz  34634  hgt750lemd  34653  knoppndvlem12  36557  knoppndvlem14  36559  knoppndvlem15  36560  knoppndvlem17  36562  knoppndvlem20  36565  poimirlem6  37666  poimirlem7  37667  poimirlem8  37668  poimirlem15  37675  poimirlem20  37680  poimirlem28  37688  opnmbllem0  37696  itg2gt0cn  37715  ftc1cnnclem  37731  ftc1anc  37741  cntotbnd  37836  3lexlogpow5ineq3  42090  3lexlogpow2ineq2  42092  3lexlogpow5ineq5  42093  aks4d1lem1  42095  0nonelalab  42100  aks4d1p1p3  42102  aks4d1p1p2  42103  aks4d1p1p4  42104  aks4d1p1p6  42106  aks4d1p1p7  42107  aks4d1p1p5  42108  aks4d1p1  42109  aks4d1p2  42110  aks4d1p3  42111  aks4d1p6  42114  aks4d1p7d1  42115  aks4d1p7  42116  aks4d1p8d3  42119  aks4d1p8  42120  2ap1caineq  42178  sticksstones1  42179  sn-addlt0d  42491  sn-addgt0d  42492  sn-mulgt1d  42512  fimgmcyc  42567  flt4lem7  42692  fltnlta  42696  pellexlem5  42866  pellfundex  42919  pellfundrp  42921  rmspecfund  42942  monotuz  42974  jm3.1lem2  43051  jm3.1lem3  43052  imo72b2  44205  prmunb2  44344  ltadd12dd  45382  infleinflem2  45409  sqrlearg  45593  lptre2pt  45678  0ellimcdiv  45687  limsup10exlem  45810  ioodvbdlimc1lem1  45969  iblspltprt  46011  itgspltprt  46017  stoweidlem7  46045  stoweidlem11  46049  stoweidlem13  46051  stoweidlem14  46052  stoweidlem26  46064  stoweidlem42  46080  stoweidlem52  46090  stoweidlem59  46097  stoweidlem60  46098  stoweidlem62  46100  wallispilem4  46106  wallispi  46108  stirlinglem1  46112  stirlinglem3  46114  stirlinglem6  46117  stirlinglem7  46118  stirlinglem10  46121  stirlinglem11  46122  dirkercncflem1  46141  dirkercncflem2  46142  fourierdlem10  46155  fourierdlem11  46156  fourierdlem12  46157  fourierdlem42  46187  fourierdlem47  46191  fourierdlem50  46194  fourierdlem51  46195  fourierdlem73  46217  fourierdlem79  46223  fourierdlem83  46227  fourierdlem103  46247  fourierdlem104  46248  sqwvfoura  46266  sqwvfourb  46267  fouriersw  46269  hoidmvlelem1  46633  hoiqssbllem2  46661  hspmbllem1  46664  pimrecltpos  46746  pimrecltneg  46762  smfaddlem1  46801  smflimlem3  46811  smflimlem4  46812  smfmullem1  46829  ormkglobd  46913  difmodm1lt  47390  fpprel2  47772  gpgedgvtx0  48092  gpgedgvtx1  48093  eenglngeehlnmlem2  48770