Theorem lelttrd 11308

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 11240	. . 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 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lt2msq1  12043  suprzcl  12590  ge0p1rp  12960  elfzolt3  13606  flflp1  13745  ltdifltdiv  13772  modsubdir  13881  seqf1olem1  13982  seqf1olem2  13983  expmulnbnd  14176  discr1  14180  faclbnd5  14239  bcp1nk  14258  hashfun  14378  swrds2  14882  abslt  15257  abs3lem  15281  fzomaxdiflem  15285  icodiamlt  15380  reccn2  15539  o1rlimmul  15561  caucvgrlem  15615  geomulcvg  15818  mertenslem1  15826  bpoly4  16001  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  sinltx  16133  eirrlem  16148  rpnnen2lem11  16168  ruclem10  16183  bitsfzolem  16380  bitsfzo  16381  bitsinv1lem  16387  smueqlem  16436  pcfaclem  16845  pockthg  16853  prmreclem5  16867  1arith  16874  4sqlem11  16902  4sqlem12  16903  4sqlem13  16904  coe1tmmul2  22195  ssblex  24349  nlmvscnlem2  24606  nlmvscnlem1  24607  nrginvrcnlem  24612  blcvx  24719  icccmplem2  24745  reconnlem2  24749  metdcnlem  24758  icopnfcnv  24873  nmoleub2lem3  25048  ipcnlem2  25177  ipcnlem1  25178  minveclem3b  25361  minveclem3  25362  pjthlem1  25370  pmltpclem2  25383  ivthlem2  25386  ovollb2lem  25422  iundisj  25482  uniioombllem3  25519  opnmbllem  25535  itg2monolem3  25686  itg2cnlem2  25696  dveflem  25916  dvferm2lem  25923  lhop1lem  25951  dvcnvre  25957  ftc1a  25977  ftc1lem4  25979  coeeulem  26162  dgradd2  26207  aaliou2b  26282  ulmdvlem1  26342  itgulm  26350  radcnvlem1  26355  radcnvlt1  26360  radcnvle  26362  psercnlem1  26368  pserdvlem1  26370  pserdv  26372  abelthlem2  26375  abelthlem7  26381  cosordlem  26472  tanord1  26479  efif1olem1  26484  logcnlem3  26586  logcnlem4  26587  efopnlem1  26598  logtayl  26602  cxpcn3lem  26690  birthdaylem3  26896  efrlim  26912  efrlimOLD  26913  lgamgulmlem2  26973  lgamucov  26981  ftalem1  27016  ftalem2  27017  ftalem5  27020  basellem1  27024  basellem3  27026  perfectlem2  27174  bposlem1  27228  bposlem3  27230  bposlem6  27233  lgsdirprm  27275  lgsqrlem2  27291  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  2sqlem8  27370  2sqblem  27375  dchrvmasumiflem1  27445  pntrmax  27508  pntlemc  27539  pntlemg  27542  pntlemr  27546  axpaschlem  28920  axlowdimlem16  28937  clwwisshclwwslem  29993  smcnlem  30676  minvecolem3  30855  pjhthlem1  31370  nmcexi  32005  iundisjf  32568  iundisjfi  32769  psgnfzto1stlem  33072  cos9thpiminplylem1  33765  dya2icoseg  34261  reprgt  34605  hgt750lem  34635  tgoldbachgtde  34644  subfaclim  35168  bcprod  35718  dnicn  36473  unbdqndv2lem1  36490  unbdqndv2lem2  36491  knoppndvlem18  36510  poimirlem6  37613  poimirlem7  37614  poimirlem12  37619  poimirlem15  37622  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  opnmbllem0  37643  mblfinlem3  37646  mblfinlem4  37647  ftc1cnnclem  37678  ftc1anclem7  37686  isbnd3  37771  cntotbnd  37783  rrnequiv  37822  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p5  42061  posbezout  42081  primrootlekpowne0  42086  aks6d1c5lem1  42117  2np3bcnp1  42125  sticksstones10  42136  sticksstones12a  42138  sticksstones22  42149  aks6d1c7lem1  42161  unitscyglem2  42177  flt4lem7  42640  fltnltalem  42643  fltnlta  42644  irrapxlem1  42803  pell14qrgapw  42857  monotoddzzfi  42924  ltrmynn0  42930  jm2.24nn  42941  acongeq  42965  jm2.26lem3  42983  jm3.1lem2  43000  binomcxplemnotnn0  44338  isosctrlem1ALT  44916  rfcnnnub  45023  zltlesub  45276  monoords  45288  supxrge  45327  infleinflem2  45360  uzubioo  45556  fmul01lt1lem1  45575  fmul01lt1lem2  45576  lptre2pt  45631  addlimc  45639  0ellimcdiv  45640  limclner  45642  climleltrp  45667  limsupubuzlem  45703  limsup10exlem  45763  icccncfext  45878  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  stoweidlem5  45996  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem25  46016  stoweidlem26  46017  stoweidlem42  46033  stoweidlem59  46050  stoweid  46054  wallispilem3  46058  wallispilem4  46059  wallispilem5  46060  fourierdlem10  46108  fourierdlem11  46109  fourierdlem12  46110  fourierdlem15  46113  fourierdlem20  46118  fourierdlem24  46122  fourierdlem30  46128  fourierdlem31  46129  fourierdlem33  46131  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem43  46141  fourierdlem44  46142  fourierdlem46  46143  fourierdlem47  46144  fourierdlem48  46145  fourierdlem50  46147  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem77  46174  fourierdlem78  46175  fourierdlem79  46176  fourierdlem87  46184  fourierdlem91  46188  fourierdlem92  46189  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem19  46244  etransclem23  46248  etransclem48  46273  ioorrnopnlem  46295  iundjiun  46451  omeiunltfirp  46510  caratheodorylem1  46517  hoicvr  46539  hoidmv1lelem2  46583  hoidmvlelem2  46587  hoiqssbllem2  46614  vonioolem1  46671  vonicclem1  46674  smflimlem4  46765  smfmullem1  46782  2tceilhalfelfzo1  47326  addmodne  47338  iccpartgt  47421  perfectALTVlem2  47716  bgoldbtbndlem2  47800  pgrple2abl  48346  logbpw2m1  48549  dignn0ldlem  48584  2itscp  48763