Theorem letr 11365

Description: Transitive law. (Contributed by NM, 12-Nov-1999.)

Assertion

Ref	Expression
letr	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11357	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1127	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 479	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11361	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11359	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1128	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 47	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 451	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 5160	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 248	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 480	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 857	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 239	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 452	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1534   ∈ wcel 2100   class class class wbr 5156  ℝcr 11164   < clt 11305   ≤ cle 11306

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 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-pre-lttri 11239  ax-pre-lttrn 11240

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 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311

This theorem is referenced by:  letri  11400  letrd  11428  le2add  11753  le2sub  11770  p1le  12120  lemul12b  12132  lemul12a  12133  zletr  12668  peano2uz2  12712  ledivge1le  13109  lemaxle  13238  elfz1b  13634  elfz0fzfz0  13670  fz0fzelfz0  13671  fz0fzdiffz0  13674  elfzmlbp  13676  difelfznle  13679  elincfzoext  13754  ssfzoulel  13790  ssfzo12bi  13791  flge  13836  flflp1  13838  fldiv4p1lem1div2  13866  fldiv4lem1div2uz2  13867  monoord  14063  le2sq2  14165  leexp2r  14204  expubnd  14207  facwordi  14318  faclbnd3  14321  facavg  14330  fi1uzind  14537  swrdswrdlem  14733  swrdccat  14764  01sqrexlem1  15268  01sqrexlem6  15273  01sqrexlem7  15274  leabs  15325  limsupbnd2  15506  rlim3  15521  lo1bdd2  15547  lo1bddrp  15548  o1lo1  15560  lo1mul  15651  lo1le  15677  isercolllem2  15691  iseraltlem2  15708  fsumabs  15826  cvgrat  15908  ruclem9  16261  algcvga  16601  prmdvdsfz  16727  prmfac1  16743  eulerthlem2  16805  modprm0  16828  prmreclem1  16939  prmreclem4  16942  4sqlem11  16978  vdwnnlem3  17020  zntoslem  21576  gsumbagdiaglemOLD  21958  gsumbagdiaglem  21961  psdmul  22182  cnllycmp  24996  evth  24999  ovoliunlem2  25546  ovolicc2lem3  25562  itg2monolem1  25794  bddiblnc  25885  coeaddlem  26299  coemullem  26300  aalioulem5  26387  aalioulem6  26388  sincosq1lem  26548  emcllem6  27052  ftalem3  27126  fsumvma2  27266  chpchtsum  27271  bcmono  27329  bposlem5  27340  gausslemma2dlem1a  27417  lgsquadlem1  27432  dchrisum0lem1  27568  pntrsumbnd2  27619  pntleml  27663  brbtwn2  28862  axlowdimlem17  28915  axlowdim  28918  crctcshwlkn0lem3  29769  crctcshwlkn0lem5  29771  wwlksubclwwlk  30014  eupth2lems  30194  nmoub3i  30729  ubthlem1  30826  ubthlem2  30827  nmopub2tALT  31865  nmfnleub2  31882  lnconi  31989  leoptr  32093  pjnmopi  32104  cdj3lem2b  32393  eulerpartlemb  34240  isbasisrelowllem1  37109  isbasisrelowllem2  37110  ltflcei  37356  itg2addnclem2  37420  itg2addnclem3  37421  itg2addnc  37422  dvasin  37452  incsequz  37496  mettrifi  37505  equivbnd  37538  bfplem1  37570  jm2.17b  42690  fmul01lt1lem2  45276  eluzge0nn0  46995  elfz2z  46998  iccpartiltu  47064  iccpartgt  47069  lighneallem2  47248