Theorem lelttrd 11281

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5095  ℝcr 11015   < clt 11156   ≤ cle 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11073  ax-pre-lttri 11090  ax-pre-lttrn 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-xr 11160  df-ltxr 11161  df-le 11162

This theorem is referenced by:  lt2msq1  12016  suprzcl  12563  ge0p1rp  12933  elfzolt3  13579  flflp1  13721  ltdifltdiv  13748  modsubdir  13857  seqf1olem1  13958  seqf1olem2  13959  expmulnbnd  14152  discr1  14156  faclbnd5  14215  bcp1nk  14234  hashfun  14354  swrds2  14857  abslt  15232  abs3lem  15256  fzomaxdiflem  15260  icodiamlt  15355  reccn2  15514  o1rlimmul  15536  caucvgrlem  15590  geomulcvg  15793  mertenslem1  15801  bpoly4  15976  ef01bndlem  16103  sin01bnd  16104  cos01bnd  16105  sinltx  16108  eirrlem  16123  rpnnen2lem11  16143  ruclem10  16158  bitsfzolem  16355  bitsfzo  16356  bitsinv1lem  16362  smueqlem  16411  pcfaclem  16820  pockthg  16828  prmreclem5  16842  1arith  16849  4sqlem11  16877  4sqlem12  16878  4sqlem13  16879  coe1tmmul2  22200  ssblex  24353  nlmvscnlem2  24610  nlmvscnlem1  24611  nrginvrcnlem  24616  blcvx  24723  icccmplem2  24749  reconnlem2  24753  metdcnlem  24762  icopnfcnv  24877  nmoleub2lem3  25052  ipcnlem2  25181  ipcnlem1  25182  minveclem3b  25365  minveclem3  25366  pjthlem1  25374  pmltpclem2  25387  ivthlem2  25390  ovollb2lem  25426  iundisj  25486  uniioombllem3  25523  opnmbllem  25539  itg2monolem3  25690  itg2cnlem2  25700  dveflem  25920  dvferm2lem  25927  lhop1lem  25955  dvcnvre  25961  ftc1a  25981  ftc1lem4  25983  coeeulem  26166  dgradd2  26211  aaliou2b  26286  ulmdvlem1  26346  itgulm  26354  radcnvlem1  26359  radcnvlt1  26364  radcnvle  26366  psercnlem1  26372  pserdvlem1  26374  pserdv  26376  abelthlem2  26379  abelthlem7  26385  cosordlem  26476  tanord1  26483  efif1olem1  26488  logcnlem3  26590  logcnlem4  26591  efopnlem1  26602  logtayl  26606  cxpcn3lem  26694  birthdaylem3  26900  efrlim  26916  efrlimOLD  26917  lgamgulmlem2  26977  lgamucov  26985  ftalem1  27020  ftalem2  27021  ftalem5  27024  basellem1  27028  basellem3  27030  perfectlem2  27178  bposlem1  27232  bposlem3  27234  bposlem6  27237  lgsdirprm  27279  lgsqrlem2  27295  lgseisen  27327  lgsquadlem1  27328  lgsquadlem2  27329  2sqlem8  27374  2sqblem  27379  dchrvmasumiflem1  27449  pntrmax  27512  pntlemc  27543  pntlemg  27546  pntlemr  27550  axpaschlem  28929  axlowdimlem16  28946  clwwisshclwwslem  30005  smcnlem  30688  minvecolem3  30867  pjhthlem1  31382  nmcexi  32017  iundisjf  32580  iundisjfi  32789  psgnfzto1stlem  33080  cos9thpiminplylem1  33806  dya2icoseg  34301  reprgt  34645  hgt750lem  34675  tgoldbachgtde  34684  subfaclim  35243  bcprod  35793  dnicn  36547  unbdqndv2lem1  36564  unbdqndv2lem2  36565  knoppndvlem18  36584  poimirlem6  37676  poimirlem7  37677  poimirlem12  37682  poimirlem15  37685  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  opnmbllem0  37706  mblfinlem3  37709  mblfinlem4  37710  ftc1cnnclem  37741  ftc1anclem7  37749  isbnd3  37834  cntotbnd  37846  rrnequiv  37885  aks4d1p1p3  42172  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p5  42183  posbezout  42203  primrootlekpowne0  42208  aks6d1c5lem1  42239  2np3bcnp1  42247  sticksstones10  42258  sticksstones12a  42260  sticksstones22  42271  aks6d1c7lem1  42283  unitscyglem2  42299  flt4lem7  42767  fltnltalem  42770  fltnlta  42771  irrapxlem1  42929  pell14qrgapw  42983  monotoddzzfi  43049  ltrmynn0  43055  jm2.24nn  43066  acongeq  43090  jm2.26lem3  43108  jm3.1lem2  43125  binomcxplemnotnn0  44463  isosctrlem1ALT  45040  rfcnnnub  45147  zltlesub  45400  monoords  45412  supxrge  45451  infleinflem2  45483  uzubioo  45679  fmul01lt1lem1  45698  fmul01lt1lem2  45699  lptre2pt  45752  addlimc  45760  0ellimcdiv  45761  limclner  45763  climleltrp  45788  limsupubuzlem  45824  limsup10exlem  45884  icccncfext  45999  ioodvbdlimc1lem1  46043  ioodvbdlimc1lem2  46044  ioodvbdlimc2lem  46046  dvnmul  46055  iblspltprt  46085  itgspltprt  46091  stoweidlem5  46117  stoweidlem11  46123  stoweidlem13  46125  stoweidlem14  46126  stoweidlem25  46137  stoweidlem26  46138  stoweidlem42  46154  stoweidlem59  46171  stoweid  46175  wallispilem3  46179  wallispilem4  46180  wallispilem5  46181  fourierdlem10  46229  fourierdlem11  46230  fourierdlem12  46231  fourierdlem15  46234  fourierdlem20  46239  fourierdlem24  46243  fourierdlem30  46249  fourierdlem31  46250  fourierdlem33  46252  fourierdlem40  46259  fourierdlem41  46260  fourierdlem42  46261  fourierdlem43  46262  fourierdlem44  46263  fourierdlem46  46264  fourierdlem47  46265  fourierdlem48  46266  fourierdlem50  46268  fourierdlem63  46281  fourierdlem64  46282  fourierdlem65  46283  fourierdlem73  46291  fourierdlem74  46292  fourierdlem75  46293  fourierdlem76  46294  fourierdlem77  46295  fourierdlem78  46296  fourierdlem79  46297  fourierdlem87  46305  fourierdlem91  46309  fourierdlem92  46310  fourierdlem103  46321  fourierdlem104  46322  fouriersw  46343  etransclem19  46365  etransclem23  46369  etransclem48  46394  ioorrnopnlem  46416  iundjiun  46572  omeiunltfirp  46631  caratheodorylem1  46638  hoicvr  46660  hoidmv1lelem2  46704  hoidmvlelem2  46708  hoiqssbllem2  46735  vonioolem1  46792  vonicclem1  46795  smflimlem4  46886  smfmullem1  46903  2tceilhalfelfzo1  47446  addmodne  47458  iccpartgt  47541  perfectALTVlem2  47836  bgoldbtbndlem2  47920  pgrple2abl  48479  logbpw2m1  48682  dignn0ldlem  48717  2itscp  48896