Theorem lelttrd 11422

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099   class class class wbr 5153  ℝcr 11157   < clt 11298   ≤ cle 11299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-pre-lttri 11232  ax-pre-lttrn 11233

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304

This theorem is referenced by:  lt2msq1  12150  suprzcl  12694  ge0p1rp  13059  elfzolt3  13696  flflp1  13827  ltdifltdiv  13854  modsubdir  13960  seqf1olem1  14061  seqf1olem2  14062  expmulnbnd  14252  discr1  14256  faclbnd5  14315  bcp1nk  14334  hashfun  14454  swrds2  14949  abslt  15319  abs3lem  15343  fzomaxdiflem  15347  icodiamlt  15440  reccn2  15599  o1rlimmul  15621  caucvgrlem  15677  geomulcvg  15880  mertenslem1  15888  bpoly4  16061  ef01bndlem  16186  sin01bnd  16187  cos01bnd  16188  sinltx  16191  eirrlem  16206  rpnnen2lem11  16226  ruclem10  16241  bitsfzolem  16434  bitsfzo  16435  bitsinv1lem  16441  smueqlem  16490  pcfaclem  16900  pockthg  16908  prmreclem5  16922  1arith  16929  4sqlem11  16957  4sqlem12  16958  4sqlem13  16959  coe1tmmul2  22267  ssblex  24425  nlmvscnlem2  24693  nlmvscnlem1  24694  nrginvrcnlem  24699  blcvx  24805  icccmplem2  24830  reconnlem2  24834  metdcnlem  24843  icopnfcnv  24958  nmoleub2lem3  25133  ipcnlem2  25263  ipcnlem1  25264  minveclem3b  25447  minveclem3  25448  pjthlem1  25456  pmltpclem2  25469  ivthlem2  25472  ovollb2lem  25508  iundisj  25568  uniioombllem3  25605  opnmbllem  25621  itg2monolem3  25773  itg2cnlem2  25783  dveflem  26002  dvferm2lem  26009  lhop1lem  26037  dvcnvre  26043  ftc1a  26063  ftc1lem4  26065  coeeulem  26251  dgradd2  26296  aaliou2b  26369  ulmdvlem1  26429  itgulm  26437  radcnvlem1  26442  radcnvlt1  26447  radcnvle  26449  psercnlem1  26455  pserdvlem1  26457  pserdv  26459  abelthlem2  26462  abelthlem7  26468  cosordlem  26557  tanord1  26564  efif1olem1  26569  logcnlem3  26671  logcnlem4  26672  efopnlem1  26683  logtayl  26687  cxpcn3lem  26775  birthdaylem3  26981  efrlim  26997  efrlimOLD  26998  lgamgulmlem2  27058  lgamucov  27066  ftalem1  27101  ftalem2  27102  ftalem5  27105  basellem1  27109  basellem3  27111  perfectlem2  27259  bposlem1  27313  bposlem3  27315  bposlem6  27318  lgsdirprm  27360  lgsqrlem2  27376  lgseisen  27408  lgsquadlem1  27409  lgsquadlem2  27410  2sqlem8  27455  2sqblem  27460  dchrvmasumiflem1  27530  pntrmax  27593  pntlemc  27624  pntlemg  27627  pntlemr  27631  axpaschlem  28874  axlowdimlem16  28891  clwwisshclwwslem  29947  smcnlem  30630  minvecolem3  30809  pjhthlem1  31324  nmcexi  31959  iundisjf  32509  iundisjfi  32698  psgnfzto1stlem  32978  dya2icoseg  34111  reprgt  34467  hgt750lem  34497  tgoldbachgtde  34506  subfaclim  35016  bcprod  35560  dnicn  36195  unbdqndv2lem1  36212  unbdqndv2lem2  36213  knoppndvlem18  36232  poimirlem6  37327  poimirlem7  37328  poimirlem12  37333  poimirlem15  37336  poimirlem17  37338  poimirlem19  37340  poimirlem20  37341  poimirlem23  37344  poimirlem24  37345  opnmbllem0  37357  mblfinlem3  37360  mblfinlem4  37361  ftc1cnnclem  37392  ftc1anclem7  37400  isbnd3  37485  cntotbnd  37497  rrnequiv  37536  aks4d1p1p3  41768  aks4d1p1p2  41769  aks4d1p1p4  41770  aks4d1p1p7  41773  aks4d1p1p5  41774  aks4d1p5  41779  posbezout  41798  primrootlekpowne0  41803  aks6d1c5lem1  41834  2np3bcnp1  41842  sticksstones10  41853  sticksstones12a  41855  sticksstones22  41866  aks6d1c7lem1  41878  metakunt1  41891  metakunt12  41902  metakunt28  41918  metakunt30  41920  flt4lem7  42313  fltnltalem  42316  fltnlta  42317  irrapxlem1  42479  pell14qrgapw  42533  monotoddzzfi  42600  ltrmynn0  42606  jm2.24nn  42617  acongeq  42641  jm2.26lem3  42659  jm3.1lem2  42676  binomcxplemnotnn0  44030  isosctrlem1ALT  44610  rfcnnnub  44635  zltlesub  44900  monoords  44912  supxrge  44953  infleinflem2  44986  uzubioo  45185  fmul01lt1lem1  45205  fmul01lt1lem2  45206  lptre2pt  45261  addlimc  45269  0ellimcdiv  45270  limclner  45272  climleltrp  45297  limsupubuzlem  45333  limsup10exlem  45393  icccncfext  45508  ioodvbdlimc1lem1  45552  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  dvnmul  45564  iblspltprt  45594  itgspltprt  45600  stoweidlem5  45626  stoweidlem11  45632  stoweidlem13  45634  stoweidlem14  45635  stoweidlem25  45646  stoweidlem26  45647  stoweidlem42  45663  stoweidlem59  45680  stoweid  45684  wallispilem3  45688  wallispilem4  45689  wallispilem5  45690  fourierdlem10  45738  fourierdlem11  45739  fourierdlem12  45740  fourierdlem15  45743  fourierdlem20  45748  fourierdlem24  45752  fourierdlem30  45758  fourierdlem31  45759  fourierdlem33  45761  fourierdlem40  45768  fourierdlem41  45769  fourierdlem42  45770  fourierdlem43  45771  fourierdlem44  45772  fourierdlem46  45773  fourierdlem47  45774  fourierdlem48  45775  fourierdlem50  45777  fourierdlem63  45790  fourierdlem64  45791  fourierdlem65  45792  fourierdlem73  45800  fourierdlem74  45801  fourierdlem75  45802  fourierdlem76  45803  fourierdlem77  45804  fourierdlem78  45805  fourierdlem79  45806  fourierdlem87  45814  fourierdlem91  45818  fourierdlem92  45819  fourierdlem103  45830  fourierdlem104  45831  fouriersw  45852  etransclem19  45874  etransclem23  45878  etransclem48  45903  ioorrnopnlem  45925  iundjiun  46081  omeiunltfirp  46140  caratheodorylem1  46147  hoicvr  46169  hoidmv1lelem2  46213  hoidmvlelem2  46217  hoiqssbllem2  46244  vonioolem1  46301  vonicclem1  46304  smflimlem4  46395  smfmullem1  46412  iccpartgt  46999  perfectALTVlem2  47294  bgoldbtbndlem2  47378  pgrple2abl  47744  logbpw2m1  47955  dignn0ldlem  47990  2itscp  48169