MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6breq Structured version   Visualization version   GIF version

Theorem syl6breq 4618
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl6breq.1 (𝜑𝐴𝑅𝐵)
syl6breq.2 𝐵 = 𝐶
Assertion
Ref Expression
syl6breq (𝜑𝐴𝑅𝐶)

Proof of Theorem syl6breq
StepHypRef Expression
1 syl6breq.1 . 2 (𝜑𝐴𝑅𝐵)
2 eqid 2609 . 2 𝐴 = 𝐴
3 syl6breq.2 . 2 𝐵 = 𝐶
41, 2, 33brtr3g 4610 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  syl6breqr  4619  difsnen  7905  marypha1lem  8200  en2eleq  8692  en2other2  8693  cda0en  8862  ackbij1lem5  8907  alephadd  9256  prlem934  9712  ltexprlem2  9716  recgt0ii  10781  discr  12821  faclbnd4lem1  12900  hashfun  13039  sqrlem7  13786  resqrex  13788  abs3lemi  13946  supcvg  14376  ege2le3  14608  cos01gt0  14709  sin02gt0  14710  bitsfzolem  14943  bitsmod  14945  prmreclem2  15408  f1otrspeq  17639  pmtrf  17647  pmtrmvd  17648  pmtrfinv  17653  efgi0  17905  efgi1  17906  dprdf1  18204  metustexhalf  22119  nlmvscnlem2  22247  icccmplem2  22382  xrge0tsms  22393  iimulcl  22492  pcoass  22580  ipcnlem2  22796  ivthlem3  22974  vitalilem4  23131  vitali  23133  dvef  23492  ply1rem  23672  aaliou3lem2  23847  abelthlem8  23942  abelthlem9  23943  cosne0  24025  sinord  24029  tanregt0  24034  argimgt0  24107  logf1o2  24141  logtayllem  24150  cxpcn3lem  24233  ang180lem2  24285  ang180lem3  24286  atanlogsublem  24387  bndatandm  24401  leibpi  24414  emcllem6  24472  emcllem7  24473  lgamgulmlem5  24504  lgamcvg2  24526  ftalem5  24548  basellem7  24558  basellem9  24560  ppieq0  24647  ppiub  24674  chpeq0  24678  chpub  24690  logfacrlim  24694  logexprlim  24695  bposlem1  24754  bposlem2  24755  lgslem3  24769  lgsquadlem1  24850  lgsquadlem3  24852  chebbnd1lem3  24905  chtppilim  24909  chpchtlim  24913  dchrvmasumiflem1  24935  dchrisum0re  24947  mudivsum  24964  mulog2sumlem2  24969  pntibndlem2  25025  pntlemb  25031  pntlemh  25033  ostth3  25072  norm3lem  27224  nmopadjlem  28166  nmopcoadji  28178  hstle  28307  stadd3i  28325  strlem5  28332  gsumle  28944  locfinreflem  29069  xrge0iifcnv  29141  carsggect  29541  omsmeas  29546  signsply0  29788  signsvtp  29820  sinccvglem  30654  faclim2  30721  poimirlem28  32431  ismblfin  32444  irrapxlem2  36229  pellexlem2  36236  areaquad  36645  dvgrat  37357  binomcxplemrat  37395  fmul01  38471  clim1fr1  38492  sinaover2ne0  38575  stoweidlem14  38731  stoweidlem16  38733  stoweidlem26  38743  stoweidlem41  38758  stoweidlem42  38759  stoweidlem45  38762  wallispi  38787  stirlinglem1  38791  stirlinglem12  38802  fourierdlem24  38848  fourierdlem107  38930  fouriersw  38948  crctcsh1wlkn0  41046  lincfsuppcl  42018  lincresunit3lem2  42085  lincresunit3  42086
  Copyright terms: Public domain W3C validator