Theorem ltletrd 11343

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
ltletrd.4	⊢ (𝜑 → 𝐴 < 𝐵)
ltletrd.5	⊢ (𝜑 → 𝐵 ≤ 𝐶)

Assertion

Ref	Expression
ltletrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		ltletr 11275	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1390	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 709	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   < clt 11216   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-pre-lttri 11147  ax-pre-lttrn 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222

This theorem is referenced by:  lelttrdi  11345  uzwo3  12944  rpgecl  13023  fznatpl1  13583  modabs  13914  seqf1olem1  14054  expgt1  14113  leexp2a  14185  bernneq3  14244  expnbnd  14245  expmulnbnd  14248  digit1  14250  discr1  14252  hashfun  14450  seqcoll2  14478  abssubne0  15344  icodiamlt  15465  reccn2  15624  isercolllem1  15692  isumltss  15878  fprodntriv  15972  efcllem  16107  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  eirrlem  16236  rpnnen2lem11  16256  ruclem10  16271  bitsmod  16470  bitsinv1lem  16475  smuval2  16516  prmreclem5  16956  1arith  16963  2expltfac  17128  mndodconglem  19581  sylow1lem1  19638  gzrngunit  21482  nlmvscnlem1  24743  nrginvrcnlem  24748  iccpnfhmeo  25004  cnheibor  25014  evth  25018  lebnumlem1  25020  ipcnlem1  25304  lmnn  25322  ovolicc2lem2  25577  itg2monolem1  25809  itg2monolem3  25811  dvferm1lem  26043  dvcnvre  26078  dvfsumlem3  26087  dvfsumrlim  26090  plyco0  26249  aaliou2b  26402  pilem2  26512  cosq34lt1  26589  cosordlem  26592  logdivlti  26682  logdivle  26684  logcnlem3  26706  logcnlem4  26707  cxpcn3lem  26809  atanre  26947  atanlogaddlem  26975  atans2  26993  birthdaylem3  27015  cxp2lim  27038  cxploglim2  27040  jensenlem2  27049  harmonicubnd  27071  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamucov  27099  ftalem2  27135  ftalem5  27138  vma1  27227  chtrpcl  27236  ppiltx  27238  fsumfldivdiaglem  27250  chtub  27273  fsumvma2  27275  chpval2  27279  chpchtsum  27280  chpub  27281  bpos1  27344  bposlem1  27345  bposlem2  27346  bposlem6  27350  gausslemma2dlem0c  27419  lgsquadlem1  27441  chebbnd1lem1  27530  chebbnd1lem2  27531  chebbnd1lem3  27532  chebbnd1  27533  chtppilimlem1  27534  chtppilimlem2  27535  chtppilim  27536  chto1ub  27537  chebbnd2  27538  chto1lb  27539  chpchtlim  27540  chpo1ub  27541  rplogsumlem2  27546  dchrisumlema  27549  dchrisumlem3  27552  dchrmusumlema  27554  dchrvmasumlem2  27559  dchrvmasumiflem1  27562  dchrisum0lema  27575  mulog2sumlem1  27595  chpdifbndlem1  27614  chpdifbnd  27616  pntrsumo1  27626  pntpbnd1  27647  pntpbnd2  27648  pntibndlem2  27652  pntlemb  27658  pntlemh  27660  pntlemr  27663  pntlem3  27670  pnt2  27674  ostth2lem1  27679  ostth2lem3  27696  ostth2lem4  27697  axsegconlem7  29121  axsegconlem10  29124  axlowdimlem16  29155  axcontlem2  29163  axcontlem4  29165  axcontlem7  29168  clwlkclwwlklem2a2  30192  clwwlkext2edg  30255  smatrcl  34090  1smat1  34098  lmdvg  34247  dya2icoseg  34571  eulerpartlems  34654  reprlt  34910  reprinfz1  34913  breprexplemc  34923  hgt750lemd  34939  hgt750lem  34942  hgt750leme  34949  tgoldbachgtde  34951  subfacval3  35536  knoppndvlem1  36947  knoppndvlem2  36948  knoppndvlem7  36953  knoppndvlem14  36960  knoppndvlem18  36964  poimirlem7  38123  poimirlem24  38140  poimirlem29  38145  mblfinlem2  38154  itg2addnclem  38167  itg2addnclem3  38169  ftc1anclem5  38193  ftc1anclem7  38195  ftc1anc  38197  areacirclem5  38208  lcmineqlem23  42665  3lexlogpow5ineq2  42669  3lexlogpow5ineq4  42670  3lexlogpow5ineq3  42671  aks4d1lem1  42676  dvrelog2  42678  aks4d1p1p3  42683  aks4d1p1p2  42684  aks4d1p1p4  42685  aks4d1p1p6  42687  aks4d1p1p7  42688  aks4d1p1p5  42689  aks4d1p1  42690  aks4d1p2  42691  aks4d1p3  42692  aks4d1p5  42694  aks4d1p6  42695  aks4d1p7d1  42696  aks4d1p7  42697  aks4d1p8d2  42699  aks4d1p8  42701  aks4d1p9  42702  posbezout  42714  hashscontpow1  42735  aks6d1c3  42737  2ap1caineq  42759  sticksstones12a  42771  sticksstones22  42782  aks6d1c7lem1  42794  aks6d1c7lem2  42795  aks6d1c7  42798  aks5lem6  42806  aks5lem8  42815  flt4lem7  43238  3cubeslem1  43262  irrapxlem4  43399  irrapxlem5  43400  pellexlem2  43404  pell14qrgapw  43450  pellqrex  43453  pellfundgt1  43457  pellfundex  43460  ltrmxnn0  43523  jm2.24nn  43533  jm2.17c  43536  jm2.24  43537  jm2.23  43570  jm3.1lem1  43591  jm3.1lem2  43592  radcnvrat  44887  dstregt0  45858  monoords  45873  uzubioo  46138  fsumnncl  46145  mullimc  46189  mullimcf  46196  sumnnodd  46203  limcleqr  46215  addlimc  46219  0ellimcdiv  46220  limclner  46222  limsupgtlem  46348  dvdivbd  46494  ioodvbdlimc1lem1  46502  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  dvnmul  46514  iblspltprt  46544  itgspltprt  46550  stoweidlem11  46582  stoweidlem24  46595  stoweidlem25  46596  stoweidlem26  46597  stoweidlem34  46605  stoweidlem36  46607  stoweidlem42  46613  stoweidlem44  46615  stoweidlem51  46622  stoweidlem59  46630  wallispi  46641  wallispi2lem1  46642  wallispi2  46644  stirlinglem11  46655  dirkertrigeqlem1  46669  dirkeritg  46673  fourierdlem10  46688  fourierdlem11  46689  fourierdlem12  46690  fourierdlem15  46693  fourierdlem19  46697  fourierdlem20  46698  fourierdlem30  46708  fourierdlem32  46710  fourierdlem40  46718  fourierdlem41  46719  fourierdlem44  46722  fourierdlem46  46723  fourierdlem47  46724  fourierdlem48  46725  fourierdlem49  46726  fourierdlem50  46727  fourierdlem63  46740  fourierdlem64  46741  fourierdlem65  46742  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem78  46755  fourierdlem79  46756  fourierdlem89  46766  fourierdlem92  46769  fourierdlem103  46780  fourierdlem104  46781  fouriersw  46802  etransclem4  46809  etransclem23  46828  etransclem31  46836  etransclem32  46837  etransclem35  46840  etransclem41  46846  etransclem48  46853  ioorrnopnlem  46875  sge0uzfsumgt  47015  sge0seq  47017  iundjiun  47031  carageniuncllem2  47093  hoidmvlelem3  47168  iunhoiioolem  47246  vonioolem1  47251  smfmullem1  47362  smfmullem2  47363  smfmullem3  47364  ceilhalfgt1  47924  modm2nep1  47963  modp2nep1  47964  modm1nep2  47965  modm1nem2  47966  modm1p1ne  47967  bgoldbtbndlem2  48425  gpgprismgrusgra  48677  gpg3nbgrvtx0  48695  gpg3kgrtriexlem1  48702  logbpw2m1  49186