Theorem ltletrd 11509

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   < clt 11382   ≤ cle 11383

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-pre-lttri 11313  ax-pre-lttrn 11314

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388

This theorem is used by:  lelttrdi  11511  uzwo3  13110  rpgecl  13190  fznatpl1  13752  modabs  14084  seqf1olem1  14224  expgt1  14283  leexp2a  14355  bernneq3  14416  expnbnd  14417  expmulnbnd  14420  digit1  14422  discr1  14424  hashfun  14623  seqcoll2  14651  abssubne0  15527  icodiamlt  15649  reccn2  15808  isercolllem1  15876  isumltss  16061  fprodntriv  16153  efcllem  16287  sin01bnd  16397  cos01bnd  16398  sin01gt0  16402  eirrlem  16416  rpnnen2lem11  16436  ruclem10  16451  bitsmod  16650  bitsinv1lem  16655  smuval2  16696  prmreclem5  17142  1arith  17149  2expltfac  17314  mndodconglem  19806  sylow1lem1  19863  gzrngunit  21793  nlmvscnlem1  25060  nrginvrcnlem  25065  iccpnfhmeo  25321  cnheibor  25331  evth  25335  lebnumlem1  25337  ipcnlem1  25621  lmnn  25639  ovolicc2lem2  25894  itg2monolem1  26126  itg2monolem3  26128  dvferm1lem  26359  dvcnvre  26394  dvfsumlem3  26403  dvfsumrlim  26406  plyco0  26565  aaliou2b  26725  pilem2  26836  cosq34lt1  26912  cosordlem  26915  logdivlti  27005  logdivle  27007  logcnlem3  27029  logcnlem4  27030  cxpcn3lem  27132  atanre  27270  atanlogaddlem  27298  atans2  27316  birthdaylem3  27338  cxp2lim  27361  cxploglim2  27363  jensenlem2  27372  harmonicubnd  27394  fsumharmonic  27396  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamucov  27422  ftalem2  27458  ftalem5  27461  vma1  27550  chtrpcl  27559  ppiltx  27561  fsumfldivdiaglem  27573  chtub  27596  fsumvma2  27598  chpval2  27602  chpchtsum  27603  chpub  27604  bpos1  27667  bposlem1  27668  bposlem2  27669  bposlem6  27673  gausslemma2dlem0c  27742  lgsquadlem1  27764  chebbnd1lem1  27853  chebbnd1lem2  27854  chebbnd1lem3  27855  chebbnd1  27856  chtppilimlem1  27857  chtppilimlem2  27858  chtppilim  27859  chto1ub  27860  chebbnd2  27861  chto1lb  27862  chpchtlim  27863  chpo1ub  27864  rplogsumlem2  27869  dchrisumlema  27872  dchrisumlem3  27875  dchrmusumlema  27877  dchrvmasumlem2  27882  dchrvmasumiflem1  27885  dchrisum0lema  27898  mulog2sumlem1  27918  chpdifbndlem1  27937  chpdifbnd  27939  pntrsumo1  27949  pntpbnd1  27970  pntpbnd2  27971  pntibndlem2  27975  pntlemb  27981  pntlemh  27983  pntlemr  27986  pntlem3  27993  pnt2  27997  ostth2lem1  28002  ostth2lem3  28019  ostth2lem4  28020  axsegconlem7  29558  axsegconlem10  29561  axlowdimlem16  29592  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  clwlkclwwlklem2a2  30641  clwwlkext2edg  30704  smatrcl  34539  1smat1  34547  lmdvg  34696  dya2icoseg  35020  eulerpartlems  35103  reprlt  35359  reprinfz1  35362  breprexplemc  35372  hgt750lemd  35388  hgt750lem  35391  hgt750leme  35398  tgoldbachgtde  35400  subfacval3  36162  knoppndvlem1  37593  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem14  37606  knoppndvlem18  37610  poimirlem7  38813  poimirlem24  38830  poimirlem29  38835  mblfinlem2  38844  itg2addnclem  38857  itg2addnclem3  38859  ftc1anclem5  38883  ftc1anclem7  38885  ftc1anc  38887  areacirclem5  38898  lcmineqlem23  43367  3lexlogpow5ineq2  43371  3lexlogpow5ineq4  43372  3lexlogpow5ineq3  43373  aks4d1lem1  43378  dvrelog2  43380  aks4d1p1p3  43385  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  aks4d1p2  43393  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8d2  43401  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  hashscontpow1  43437  aks6d1c3  43439  2ap1caineq  43461  sticksstones12a  43473  sticksstones22  43484  aks6d1c7lem1  43496  aks6d1c7lem2  43497  aks6d1c7  43500  aks5lem6  43508  aks5lem8  43517  3cubeslem1  43960  irrapxlem4  44098  irrapxlem5  44099  pellexlem2  44103  pell14qrgapw  44149  pellqrex  44152  pellfundgt1  44156  pellfundex  44159  ltrmxnn0  44222  jm2.24nn  44232  jm2.17c  44235  jm2.24  44236  jm2.23  44269  jm3.1lem1  44290  jm3.1lem2  44291  radcnvrat  45559  dstregt0  46571  monoords  46586  uzubioo  46850  fsumnncl  46857  mullimc  46901  mullimcf  46908  sumnnodd  46915  limcleqr  46927  addlimc  46931  0ellimcdiv  46932  limclner  46934  limsupgtlem  47060  dvdivbd  47206  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnmul  47226  iblspltprt  47256  itgspltprt  47262  stoweidlem11  47294  stoweidlem24  47307  stoweidlem25  47308  stoweidlem26  47309  stoweidlem34  47317  stoweidlem36  47319  stoweidlem42  47325  stoweidlem44  47327  stoweidlem51  47334  stoweidlem59  47342  wallispi  47353  wallispi2lem1  47354  wallispi2  47356  stirlinglem11  47367  dirkertrigeqlem1  47381  dirkeritg  47385  fourierdlem10  47400  fourierdlem11  47401  fourierdlem12  47402  fourierdlem15  47405  fourierdlem19  47409  fourierdlem20  47410  fourierdlem30  47420  fourierdlem32  47422  fourierdlem40  47430  fourierdlem41  47431  fourierdlem44  47434  fourierdlem46  47435  fourierdlem47  47436  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem78  47467  fourierdlem79  47468  fourierdlem89  47478  fourierdlem92  47481  fourierdlem103  47492  fourierdlem104  47493  fouriersw  47514  etransclem4  47521  etransclem23  47540  etransclem31  47548  etransclem32  47549  etransclem35  47552  etransclem41  47558  etransclem48  47565  ioorrnopnlem  47587  sge0uzfsumgt  47727  sge0seq  47729  iundjiun  47743  carageniuncllem2  47805  hoidmvlelem3  47880  iunhoiioolem  47958  vonioolem1  47963  smfmullem1  48074  smfmullem2  48075  smfmullem3  48076  ceilhalfgt1  48676  modm2nep1  48715  modp2nep1  48716  modm1nep2  48717  modm1nem2  48718  modm1p1ne  48719  bgoldbtbndlem2  49177  gpgprismgrusgra  49429  gpg3nbgrvtx0  49447  gpg3kgrtriexlem1  49454  logbpw2m1  50010