Theorem letr 11300

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11292	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1146	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 485	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11296	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11294	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1147	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 48	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 457	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 5114	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 252	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 486	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 872	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 243	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 458	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095   < clt 11239   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-pre-lttri 11170  ax-pre-lttrn 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  letri  11335  letrd  11363  le2add  11692  le2sub  11709  p1le  12056  lemul12b  12068  lemul12a  12069  zletr  12634  peano2uz2  12680  ledivge1le  13085  lemaxle  13217  elfz1b  13617  elfz0fzfz0  13657  fz0fzelfz0  13658  fz0fzdiffz0  13661  elfzmlbp  13663  difelfznle  13666  elincfzoext  13748  ssfzoulel  13785  ssfzo12bi  13786  flge  13834  flflp1  13836  fldiv4p1lem1div2  13864  fldiv4lem1div2uz2  13865  monoord  14064  le2sq2  14167  leexp2r  14206  expubnd  14210  facwordi  14321  faclbnd3  14324  facavg  14333  fi1uzind  14540  swrdswrdlem  14737  swrdccat  14768  01sqrexlem1  15289  01sqrexlem6  15294  01sqrexlem7  15295  leabs  15346  limsupbnd2  15530  rlim3  15545  lo1bdd2  15571  lo1bddrp  15572  o1lo1  15584  lo1mul  15675  lo1le  15699  isercolllem2  15713  iseraltlem2  15730  fsumabs  15849  cvgrat  15933  ruclem9  16290  algcvga  16633  prmdvdsfz  16760  prmfac1  16775  eulerthlem2  16837  modprm0  16861  prmreclem1  16972  prmreclem4  16975  4sqlem11  17011  vdwnnlem3  17053  zntoslem  21671  gsumbagdiaglem  22046  psdmul  22294  cnllycmp  25080  evth  25083  ovoliunlem2  25627  ovolicc2lem3  25643  itg2monolem1  25874  bddiblnc  25966  coeaddlem  26371  coemullem  26372  aalioulem5  26462  aalioulem6  26463  sincosq1lem  26624  emcllem6  27127  ftalem3  27201  fsumvma2  27340  chpchtsum  27345  bcmono  27403  bposlem5  27414  gausslemma2dlem1a  27491  lgsquadlem1  27506  dchrisum0lem1  27642  pntrsumbnd2  27693  pntleml  27737  brbtwn2  29192  axlowdimlem17  29245  axlowdim  29248  crctcshwlkn0lem3  30098  crctcshwlkn0lem5  30100  wwlksubclwwlk  30346  eupth2lems  30526  nmoub3i  31062  ubthlem1  31159  ubthlem2  31160  nmopub2tALT  32198  nmfnleub2  32215  lnconi  32322  leoptr  32426  pjnmopi  32437  cdj3lem2b  32726  eulerpartlemb  34699  isbasisrelowllem1  37884  isbasisrelowllem2  37885  ltflcei  38142  itg2addnclem2  38206  itg2addnclem3  38207  itg2addnc  38208  dvasin  38238  incsequz  38282  mettrifi  38291  equivbnd  38324  bfplem1  38356  jm2.17b  43573  fmul01lt1lem2  46186  eluzge0nn0  47931  elfz2z  47934  iccpartiltu  48053  iccpartgt  48058  lighneallem2  48240