Theorem lttrd 10793

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2107   class class class wbr 5057  ℝcr 10528   < clt 10667

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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-pre-lttrn 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672

This theorem is referenced by:  nnne0  11663  expgt1  13459  ltexp2a  13522  expcan  13525  ltexp2  13526  leexp2  13527  expnlbnd2  13587  expmulnbnd  13588  reccn2  14945  efgt1  15461  tanhlt1  15505  ruclem2  15577  isprm7  16044  pythagtriplem13  16156  fldivp1  16225  4sqlem12  16284  sylow1lem1  18715  telgsums  19105  chfacffsupp  21456  chfacfscmul0  21458  chfacfpmmul0  21462  nrginvrcnlem  23292  iccntr  23421  icccmplem2  23423  opnreen  23431  pjthlem1  24032  pmltpclem2  24042  ovollb2lem  24081  opnmbllem  24194  volivth  24200  lhop1lem  24602  dvcnvrelem1  24606  dvcvx  24609  ftc1lem4  24628  aaliou3lem7  24930  ulmdvlem1  24980  reeff1olem  25026  pilem2  25032  pilem3  25033  tangtx  25083  tanord1  25113  tanord  25114  rplogcl  25179  logimul  25189  logcnlem3  25219  efopnlem1  25231  cxplt  25269  cxple  25270  cxpcn3lem  25320  asinsin  25462  atanlogaddlem  25483  atanlogsublem  25485  cxp2limlem  25545  cxp2lim  25546  zetacvg  25584  lgamucov  25607  lgamcvg2  25624  ftalem1  25642  mersenne  25795  bposlem2  25853  bposlem6  25857  bposlem9  25860  lgsqrlem2  25915  lgsquadlem2  25949  chebbnd1lem2  26038  chebbnd1lem3  26039  chebbnd1  26040  chtppilimlem1  26041  chto1ub  26044  mulog2sumlem2  26103  chpdifbndlem1  26121  selberg3lem1  26125  pntrlog2bndlem2  26146  pntrlog2bndlem4  26148  pntpbnd1a  26153  pntpbnd1  26154  pntpbnd2  26155  pntibndlem1  26157  pntibndlem2  26159  pntibndlem3  26160  pntibnd  26161  pntlemb  26165  pntlemr  26170  pntlemf  26173  pnt  26182  ostth2lem1  26186  ostth2lem3  26203  ostth2lem4  26204  wwlksext2clwwlk  27828  frgrogt3nreg  28168  friendshipgt3  28169  pjhthlem1  29160  psgnfzto1stlem  30735  1smat1  31062  sqsscirc1  31144  xrge0iifiso  31171  sgnsub  31795  signslema  31825  chtvalz  31893  hgt750lemd  31912  knoppndvlem12  33855  knoppndvlem14  33857  knoppndvlem15  33858  knoppndvlem17  33860  knoppndvlem20  33863  poimirlem6  34890  poimirlem7  34891  poimirlem8  34892  poimirlem15  34899  poimirlem20  34904  poimirlem28  34912  opnmbllem0  34920  itg2gt0cn  34939  ftc1cnnclem  34957  ftc1anc  34967  cntotbnd  35066  fltnlta  39265  pellexlem5  39420  pellfundex  39473  pellfundrp  39475  rmspecfund  39496  monotuz  39528  jm3.1lem2  39605  jm3.1lem3  39606  imo72b2  40515  prmunb2  40633  neglt  41539  ltadd12dd  41600  infleinflem2  41628  sqrlearg  41818  lptre2pt  41910  0ellimcdiv  41919  limsup10exlem  42042  ioodvbdlimc1lem1  42205  iblspltprt  42247  itgspltprt  42253  stoweidlem7  42282  stoweidlem11  42286  stoweidlem13  42288  stoweidlem14  42289  stoweidlem26  42301  stoweidlem42  42317  stoweidlem52  42327  stoweidlem59  42334  stoweidlem60  42335  stoweidlem62  42337  wallispilem4  42343  wallispi  42345  stirlinglem1  42349  stirlinglem3  42351  stirlinglem6  42354  stirlinglem7  42355  stirlinglem10  42358  stirlinglem11  42359  dirkercncflem1  42378  dirkercncflem2  42379  fourierdlem10  42392  fourierdlem11  42393  fourierdlem12  42394  fourierdlem42  42424  fourierdlem47  42428  fourierdlem50  42431  fourierdlem51  42432  fourierdlem73  42454  fourierdlem79  42460  fourierdlem83  42464  fourierdlem103  42484  fourierdlem104  42485  sqwvfoura  42503  sqwvfourb  42504  fouriersw  42506  hoidmvlelem1  42867  hoiqssbllem2  42895  hspmbllem1  42898  pimrecltpos  42977  pimrecltneg  42991  smfaddlem1  43029  smflimlem3  43039  smflimlem4  43040  smfmullem1  43056  fpprel2  43896  eenglngeehlnmlem2  44715