Theorem letr 11305

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11297	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1148	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 485	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11301	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11299	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1149	. . . . . 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 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5110  ℝcr 11100   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  letri  11340  letrd  11368  le2add  11697  le2sub  11714  p1le  12061  lemul12b  12073  lemul12a  12074  zletr  12639  peano2uz2  12685  ledivge1le  13090  lemaxle  13222  elfz1b  13623  elfz0fzfz0  13663  fz0fzelfz0  13664  fz0fzdiffz0  13667  elfzmlbp  13669  difelfznle  13672  elincfzoext  13754  ssfzoulel  13791  ssfzo12bi  13792  flge  13840  flflp1  13842  fldiv4p1lem1div2  13870  fldiv4lem1div2uz2  13871  monoord  14070  le2sq2  14173  leexp2r  14212  expubnd  14216  facwordi  14327  faclbnd3  14330  facavg  14339  fi1uzind  14546  swrdswrdlem  14743  swrdccat  14774  01sqrexlem1  15295  01sqrexlem6  15300  01sqrexlem7  15301  leabs  15352  limsupbnd2  15536  rlim3  15551  lo1bdd2  15577  lo1bddrp  15578  o1lo1  15590  lo1mul  15681  lo1le  15705  isercolllem2  15719  iseraltlem2  15736  fsumabs  15855  cvgrat  15939  ruclem9  16295  algcvga  16638  prmdvdsfz  16765  prmfac1  16780  eulerthlem2  16842  modprm0  16866  prmreclem1  16977  prmreclem4  16980  4sqlem11  17016  vdwnnlem3  17058  zntoslem  21687  gsumbagdiaglem  22062  psdmul  22310  cnllycmp  25096  evth  25099  ovoliunlem2  25643  ovolicc2lem3  25659  itg2monolem1  25890  bddiblnc  25982  coeaddlem  26387  coemullem  26388  aalioulem5  26480  aalioulem6  26481  sincosq1lem  26643  emcllem6  27146  ftalem3  27220  fsumvma2  27359  chpchtsum  27364  bcmono  27422  bposlem5  27433  gausslemma2dlem1a  27510  lgsquadlem1  27525  dchrisum0lem1  27661  pntrsumbnd2  27712  pntleml  27756  brbtwn2  29236  axlowdimlem17  29289  axlowdim  29292  crctcshwlkn0lem3  30142  crctcshwlkn0lem5  30144  wwlksubclwwlk  30390  eupth2lems  30570  nmoub3i  31106  ubthlem1  31203  ubthlem2  31204  nmopub2tALT  32242  nmfnleub2  32259  lnconi  32366  leoptr  32470  pjnmopi  32481  cdj3lem2b  32770  eulerpartlemb  34739  isbasisrelowllem1  37982  isbasisrelowllem2  37983  ltflcei  38240  itg2addnclem2  38304  itg2addnclem3  38305  itg2addnc  38306  dvasin  38336  incsequz  38380  mettrifi  38389  equivbnd  38422  bfplem1  38454  jm2.17b  43671  fmul01lt1lem2  46284  eluzge0nn0  48032  elfz2z  48035  iccpartiltu  48154  iccpartgt  48159  lighneallem2  48341