Theorem lelttrd 11448

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is referenced by:  lt2msq1  12179  suprzcl  12723  ge0p1rp  13088  elfzolt3  13726  flflp1  13858  ltdifltdiv  13885  modsubdir  13991  seqf1olem1  14092  seqf1olem2  14093  expmulnbnd  14284  discr1  14288  faclbnd5  14347  bcp1nk  14366  hashfun  14486  swrds2  14989  abslt  15363  abs3lem  15387  fzomaxdiflem  15391  icodiamlt  15484  reccn2  15643  o1rlimmul  15665  caucvgrlem  15721  geomulcvg  15924  mertenslem1  15932  bpoly4  16107  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sinltx  16237  eirrlem  16252  rpnnen2lem11  16272  ruclem10  16287  bitsfzolem  16480  bitsfzo  16481  bitsinv1lem  16487  smueqlem  16536  pcfaclem  16945  pockthg  16953  prmreclem5  16967  1arith  16974  4sqlem11  17002  4sqlem12  17003  4sqlem13  17004  coe1tmmul2  22300  ssblex  24459  nlmvscnlem2  24727  nlmvscnlem1  24728  nrginvrcnlem  24733  blcvx  24839  icccmplem2  24864  reconnlem2  24868  metdcnlem  24877  icopnfcnv  24992  nmoleub2lem3  25167  ipcnlem2  25297  ipcnlem1  25298  minveclem3b  25481  minveclem3  25482  pjthlem1  25490  pmltpclem2  25503  ivthlem2  25506  ovollb2lem  25542  iundisj  25602  uniioombllem3  25639  opnmbllem  25655  itg2monolem3  25807  itg2cnlem2  25817  dveflem  26037  dvferm2lem  26044  lhop1lem  26072  dvcnvre  26078  ftc1a  26098  ftc1lem4  26100  coeeulem  26283  dgradd2  26328  aaliou2b  26401  ulmdvlem1  26461  itgulm  26469  radcnvlem1  26474  radcnvlt1  26479  radcnvle  26481  psercnlem1  26487  pserdvlem1  26489  pserdv  26491  abelthlem2  26494  abelthlem7  26500  cosordlem  26590  tanord1  26597  efif1olem1  26602  logcnlem3  26704  logcnlem4  26705  efopnlem1  26716  logtayl  26720  cxpcn3lem  26808  birthdaylem3  27014  efrlim  27030  efrlimOLD  27031  lgamgulmlem2  27091  lgamucov  27099  ftalem1  27134  ftalem2  27135  ftalem5  27138  basellem1  27142  basellem3  27144  perfectlem2  27292  bposlem1  27346  bposlem3  27348  bposlem6  27351  lgsdirprm  27393  lgsqrlem2  27409  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  2sqlem8  27488  2sqblem  27493  dchrvmasumiflem1  27563  pntrmax  27626  pntlemc  27657  pntlemg  27660  pntlemr  27664  axpaschlem  28973  axlowdimlem16  28990  clwwisshclwwslem  30046  smcnlem  30729  minvecolem3  30908  pjhthlem1  31423  nmcexi  32058  iundisjf  32611  iundisjfi  32801  psgnfzto1stlem  33093  dya2icoseg  34242  reprgt  34598  hgt750lem  34628  tgoldbachgtde  34637  subfaclim  35156  bcprod  35700  dnicn  36458  unbdqndv2lem1  36475  unbdqndv2lem2  36476  knoppndvlem18  36495  poimirlem6  37586  poimirlem7  37587  poimirlem12  37592  poimirlem15  37595  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  ftc1cnnclem  37651  ftc1anclem7  37659  isbnd3  37744  cntotbnd  37756  rrnequiv  37795  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p5  42037  posbezout  42057  primrootlekpowne0  42062  aks6d1c5lem1  42093  2np3bcnp1  42101  sticksstones10  42112  sticksstones12a  42114  sticksstones22  42125  aks6d1c7lem1  42137  unitscyglem2  42153  metakunt1  42162  metakunt12  42173  metakunt28  42189  metakunt30  42191  flt4lem7  42614  fltnltalem  42617  fltnlta  42618  irrapxlem1  42778  pell14qrgapw  42832  monotoddzzfi  42899  ltrmynn0  42905  jm2.24nn  42916  acongeq  42940  jm2.26lem3  42958  jm3.1lem2  42975  binomcxplemnotnn0  44325  isosctrlem1ALT  44905  rfcnnnub  44936  zltlesub  45200  monoords  45212  supxrge  45253  infleinflem2  45286  uzubioo  45485  fmul01lt1lem1  45505  fmul01lt1lem2  45506  lptre2pt  45561  addlimc  45569  0ellimcdiv  45570  limclner  45572  climleltrp  45597  limsupubuzlem  45633  limsup10exlem  45693  icccncfext  45808  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  stoweidlem5  45926  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem25  45946  stoweidlem26  45947  stoweidlem42  45963  stoweidlem59  45980  stoweid  45984  wallispilem3  45988  wallispilem4  45989  wallispilem5  45990  fourierdlem10  46038  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem20  46048  fourierdlem24  46052  fourierdlem30  46058  fourierdlem31  46059  fourierdlem33  46061  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem43  46071  fourierdlem44  46072  fourierdlem46  46073  fourierdlem47  46074  fourierdlem48  46075  fourierdlem50  46077  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem77  46104  fourierdlem78  46105  fourierdlem79  46106  fourierdlem87  46114  fourierdlem91  46118  fourierdlem92  46119  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  etransclem19  46174  etransclem23  46178  etransclem48  46203  ioorrnopnlem  46225  iundjiun  46381  omeiunltfirp  46440  caratheodorylem1  46447  hoicvr  46469  hoidmv1lelem2  46513  hoidmvlelem2  46517  hoiqssbllem2  46544  vonioolem1  46601  vonicclem1  46604  smflimlem4  46695  smfmullem1  46712  iccpartgt  47301  perfectALTVlem2  47596  bgoldbtbndlem2  47680  pgrple2abl  48090  logbpw2m1  48301  dignn0ldlem  48336  2itscp  48515