Theorem lelttrd 11339

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

Hypotheses

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

Assertion

Ref	Expression
lelttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lelttrd

Step	Hyp	Ref	Expression
1		lelttrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		lelttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lelttr 11271	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  lt2msq1  12074  suprzcl  12621  ge0p1rp  12991  elfzolt3  13637  flflp1  13776  ltdifltdiv  13803  modsubdir  13912  seqf1olem1  14013  seqf1olem2  14014  expmulnbnd  14207  discr1  14211  faclbnd5  14270  bcp1nk  14289  hashfun  14409  swrds2  14913  abslt  15288  abs3lem  15312  fzomaxdiflem  15316  icodiamlt  15411  reccn2  15570  o1rlimmul  15592  caucvgrlem  15646  geomulcvg  15849  mertenslem1  15857  bpoly4  16032  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sinltx  16164  eirrlem  16179  rpnnen2lem11  16199  ruclem10  16214  bitsfzolem  16411  bitsfzo  16412  bitsinv1lem  16418  smueqlem  16467  pcfaclem  16876  pockthg  16884  prmreclem5  16898  1arith  16905  4sqlem11  16933  4sqlem12  16934  4sqlem13  16935  coe1tmmul2  22169  ssblex  24323  nlmvscnlem2  24580  nlmvscnlem1  24581  nrginvrcnlem  24586  blcvx  24693  icccmplem2  24719  reconnlem2  24723  metdcnlem  24732  icopnfcnv  24847  nmoleub2lem3  25022  ipcnlem2  25151  ipcnlem1  25152  minveclem3b  25335  minveclem3  25336  pjthlem1  25344  pmltpclem2  25357  ivthlem2  25360  ovollb2lem  25396  iundisj  25456  uniioombllem3  25493  opnmbllem  25509  itg2monolem3  25660  itg2cnlem2  25670  dveflem  25890  dvferm2lem  25897  lhop1lem  25925  dvcnvre  25931  ftc1a  25951  ftc1lem4  25953  coeeulem  26136  dgradd2  26181  aaliou2b  26256  ulmdvlem1  26316  itgulm  26324  radcnvlem1  26329  radcnvlt1  26334  radcnvle  26336  psercnlem1  26342  pserdvlem1  26344  pserdv  26346  abelthlem2  26349  abelthlem7  26355  cosordlem  26446  tanord1  26453  efif1olem1  26458  logcnlem3  26560  logcnlem4  26561  efopnlem1  26572  logtayl  26576  cxpcn3lem  26664  birthdaylem3  26870  efrlim  26886  efrlimOLD  26887  lgamgulmlem2  26947  lgamucov  26955  ftalem1  26990  ftalem2  26991  ftalem5  26994  basellem1  26998  basellem3  27000  perfectlem2  27148  bposlem1  27202  bposlem3  27204  bposlem6  27207  lgsdirprm  27249  lgsqrlem2  27265  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  2sqlem8  27344  2sqblem  27349  dchrvmasumiflem1  27419  pntrmax  27482  pntlemc  27513  pntlemg  27516  pntlemr  27520  axpaschlem  28874  axlowdimlem16  28891  clwwisshclwwslem  29950  smcnlem  30633  minvecolem3  30812  pjhthlem1  31327  nmcexi  31962  iundisjf  32525  iundisjfi  32726  psgnfzto1stlem  33064  cos9thpiminplylem1  33779  dya2icoseg  34275  reprgt  34619  hgt750lem  34649  tgoldbachgtde  34658  subfaclim  35182  bcprod  35732  dnicn  36487  unbdqndv2lem1  36504  unbdqndv2lem2  36505  knoppndvlem18  36524  poimirlem6  37627  poimirlem7  37628  poimirlem12  37633  poimirlem15  37636  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  ftc1cnnclem  37692  ftc1anclem7  37700  isbnd3  37785  cntotbnd  37797  rrnequiv  37836  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p5  42075  posbezout  42095  primrootlekpowne0  42100  aks6d1c5lem1  42131  2np3bcnp1  42139  sticksstones10  42150  sticksstones12a  42152  sticksstones22  42163  aks6d1c7lem1  42175  unitscyglem2  42191  flt4lem7  42654  fltnltalem  42657  fltnlta  42658  irrapxlem1  42817  pell14qrgapw  42871  monotoddzzfi  42938  ltrmynn0  42944  jm2.24nn  42955  acongeq  42979  jm2.26lem3  42997  jm3.1lem2  43014  binomcxplemnotnn0  44352  isosctrlem1ALT  44930  rfcnnnub  45037  zltlesub  45290  monoords  45302  supxrge  45341  infleinflem2  45374  uzubioo  45570  fmul01lt1lem1  45589  fmul01lt1lem2  45590  lptre2pt  45645  addlimc  45653  0ellimcdiv  45654  limclner  45656  climleltrp  45681  limsupubuzlem  45717  limsup10exlem  45777  icccncfext  45892  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  stoweidlem5  46010  stoweidlem11  46016  stoweidlem13  46018  stoweidlem14  46019  stoweidlem25  46030  stoweidlem26  46031  stoweidlem42  46047  stoweidlem59  46064  stoweid  46068  wallispilem3  46072  wallispilem4  46073  wallispilem5  46074  fourierdlem10  46122  fourierdlem11  46123  fourierdlem12  46124  fourierdlem15  46127  fourierdlem20  46132  fourierdlem24  46136  fourierdlem30  46142  fourierdlem31  46143  fourierdlem33  46145  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem43  46155  fourierdlem44  46156  fourierdlem46  46157  fourierdlem47  46158  fourierdlem48  46159  fourierdlem50  46161  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem77  46188  fourierdlem78  46189  fourierdlem79  46190  fourierdlem87  46198  fourierdlem91  46202  fourierdlem92  46203  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  etransclem19  46258  etransclem23  46262  etransclem48  46287  ioorrnopnlem  46309  iundjiun  46465  omeiunltfirp  46524  caratheodorylem1  46531  hoicvr  46553  hoidmv1lelem2  46597  hoidmvlelem2  46601  hoiqssbllem2  46628  vonioolem1  46685  vonicclem1  46688  smflimlem4  46779  smfmullem1  46796  2tceilhalfelfzo1  47337  addmodne  47349  iccpartgt  47432  perfectALTVlem2  47727  bgoldbtbndlem2  47811  pgrple2abl  48357  logbpw2m1  48560  dignn0ldlem  48595  2itscp  48774