Theorem lttrd 11395

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123   < clt 11267

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttrn 11199

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is used by:  mulgt1  12100  nnne0  12294  neglt  13062  expgt1  14164  ltexp2a  14230  expcan  14233  ltexp2  14234  leexp2  14235  expnlbnd2  14298  expmulnbnd  14299  sgnsub  15179  reccn2  15684  efgt1  16204  tanhlt1  16248  ruclem2  16320  isprm7  16799  pythagtriplem13  16919  fldivp1  16989  4sqlem12  17048  chnub  18710  chnccat  18714  sylow1lem1  19725  telgsums  20120  chfacffsupp  23081  chfacfscmul0  23083  chfacfpmmul0  23087  nrginvrcnlem  24917  iccntr  25048  icccmplem2  25050  opnreen  25058  pjthlem1  25665  pmltpclem2  25677  ovollb2lem  25716  opnmbllem  25829  volivth  25835  lhop1lem  26240  dvcnvrelem1  26244  dvcvx  26247  ftc1lem4  26266  aaliou3lem7  26585  ulmdvlem1  26636  reeff1olem  26682  pilem2  26688  pilem3  26689  tangtx  26743  tanord1  26774  tanord  26775  rplogcl  26841  logimul  26851  logcnlem3  26881  efopnlem1  26893  cxplt  26931  cxple  26932  cxpcn3lem  26984  asinsin  27129  atanlogaddlem  27150  atanlogsublem  27152  cxp2limlem  27212  cxp2lim  27213  zetacvg  27251  lgamucov  27274  lgamcvg2  27291  ftalem1  27309  mersenne  27463  bposlem2  27521  bposlem6  27525  bposlem9  27528  lgsqrlem2  27583  lgsquadlem2  27617  chebbnd1lem2  27706  chebbnd1lem3  27707  chebbnd1  27708  chtppilimlem1  27709  chto1ub  27712  mulog2sumlem2  27771  chpdifbndlem1  27789  selberg3lem1  27793  pntrlog2bndlem2  27814  pntrlog2bndlem4  27816  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntibndlem1  27825  pntibndlem2  27827  pntibndlem3  27828  pntibnd  27829  pntlemb  27833  pntlemr  27838  pntlemf  27841  pnt  27850  ostth2lem1  27854  ostth2lem3  27871  ostth2lem4  27872  wwlksext2clwwlk  30527  frgrogt3nreg  30877  friendshipgt3  30878  pjhthlem1  31872  psgnfzto1stlem  33540  1smat1  34314  sqsscirc1  34418  xrge0iifiso  34445  signslema  35070  chtvalz  35137  hgt750lemd  35156  knoppndvlem12  37220  knoppndvlem14  37222  knoppndvlem15  37223  knoppndvlem17  37225  knoppndvlem20  37228  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem15  38384  poimirlem20  38389  poimirlem28  38397  opnmbllem0  38405  itg2gt0cn  38424  ftc1cnnclem  38440  ftc1anc  38450  cntotbnd  38546  3lexlogpow5ineq3  42923  3lexlogpow2ineq2  42925  3lexlogpow5ineq5  42926  aks4d1lem1  42928  0nonelalab  42933  aks4d1p1p3  42935  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8d3  42952  aks4d1p8  42953  2ap1caineq  43011  sticksstones1  43012  sn-addlt0d  43346  sn-addgt0d  43347  sn-mulgt1d  43367  fimgmcyc  43416  flt4lem7  43505  fltnlta  43509  pellexlem5  43674  pellfundex  43727  pellfundrp  43729  rmspecfund  43750  monotuz  43782  jm3.1lem2  43859  jm3.1lem3  43860  imo72b2  45012  prmunb2  45135  ltadd12dd  46173  infleinflem2  46200  sqrlearg  46383  lptre2pt  46468  0ellimcdiv  46477  limsup10exlem  46600  ioodvbdlimc1lem1  46759  iblspltprt  46801  itgspltprt  46807  stoweidlem7  46835  stoweidlem11  46839  stoweidlem13  46841  stoweidlem14  46842  stoweidlem26  46854  stoweidlem42  46870  stoweidlem52  46880  stoweidlem59  46887  stoweidlem60  46888  stoweidlem62  46890  wallispilem4  46896  wallispi  46898  stirlinglem1  46902  stirlinglem3  46904  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  stirlinglem11  46912  dirkercncflem1  46931  dirkercncflem2  46932  fourierdlem10  46945  fourierdlem11  46946  fourierdlem12  46947  fourierdlem42  46977  fourierdlem47  46981  fourierdlem50  46984  fourierdlem51  46985  fourierdlem73  47007  fourierdlem79  47013  fourierdlem83  47017  fourierdlem103  47037  fourierdlem104  47038  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  hoidmvlelem1  47423  hoiqssbllem2  47451  hspmbllem1  47454  pimrecltpos  47536  pimrecltneg  47552  smfaddlem1  47591  smflimlem3  47601  smflimlem4  47602  smfmullem1  47619  ormkglobd  47705  chnsubseq  47708  difmodm1lt  48253  2timesltsqm1  48267  fpprel2  48657  gpgedgvtx0  48977  gpgedgvtx1  48978  eenglngeehlnmlem2  49668