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

Theorem syl6breq 4726
 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 2651 . 2 𝐴 = 𝐴
3 syl6breq.2 . 2 𝐵 = 𝐶
41, 2, 33brtr3g 4718 1 (𝜑𝐴𝑅𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523   class class class wbr 4685 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686 This theorem is referenced by:  syl6breqr  4727  difsnen  8083  marypha1lem  8380  en2eleq  8869  en2other2  8870  cda0en  9039  ackbij1lem5  9084  alephadd  9437  prlem934  9893  ltexprlem2  9897  recgt0ii  10967  discr  13041  faclbnd4lem1  13120  hashfun  13262  sqrlem7  14033  resqrex  14035  abs3lemi  14193  supcvg  14632  ege2le3  14864  cos01gt0  14965  sin02gt0  14966  bitsfzolem  15203  bitsmod  15205  prmreclem2  15668  f1otrspeq  17913  pmtrf  17921  pmtrmvd  17922  pmtrfinv  17927  efgi0  18179  efgi1  18180  dprdf1  18478  metustexhalf  22408  nlmvscnlem2  22536  icccmplem2  22673  xrge0tsms  22684  iimulcl  22783  pcoass  22870  ipcnlem2  23089  ivthlem3  23268  vitalilem4  23425  vitali  23427  dvef  23788  ply1rem  23968  aaliou3lem2  24143  abelthlem8  24238  abelthlem9  24239  cosne0  24321  sinord  24325  tanregt0  24330  argimgt0  24403  logf1o2  24441  logtayllem  24450  cxpcn3lem  24533  ang180lem2  24585  ang180lem3  24586  atanlogsublem  24687  bndatandm  24701  leibpi  24714  emcllem6  24772  emcllem7  24773  lgamgulmlem5  24804  lgamcvg2  24826  ftalem5  24848  basellem7  24858  basellem9  24860  ppieq0  24947  ppiub  24974  chpeq0  24978  chpub  24990  logfacrlim  24994  logexprlim  24995  bposlem1  25054  bposlem2  25055  lgslem3  25069  lgsquadlem1  25150  lgsquadlem3  25152  chebbnd1lem3  25205  chtppilim  25209  chpchtlim  25213  dchrvmasumiflem1  25235  dchrisum0re  25247  mudivsum  25264  mulog2sumlem2  25269  pntibndlem2  25325  pntlemb  25331  pntlemh  25333  ostth3  25372  crctcshwlkn0  26769  norm3lem  28134  nmopadjlem  29076  nmopcoadji  29088  hstle  29217  stadd3i  29235  strlem5  29242  gsumle  29907  locfinreflem  30035  xrge0iifcnv  30107  carsggect  30508  omsmeas  30513  signsply0  30756  signsvtp  30788  tgoldbachgtd  30868  sinccvglem  31692  faclim2  31760  poimirlem28  33567  ismblfin  33580  irrapxlem2  37704  pellexlem2  37711  areaquad  38119  dvgrat  38828  binomcxplemrat  38866  fmul01  40130  clim1fr1  40151  sinaover2ne0  40397  stoweidlem14  40549  stoweidlem16  40551  stoweidlem26  40561  stoweidlem41  40576  stoweidlem42  40577  stoweidlem45  40580  wallispi  40605  stirlinglem1  40609  stirlinglem12  40620  fourierdlem24  40666  fourierdlem107  40748  fouriersw  40766  meaiunincf  41018  meaiuninc3  41020  lincfsuppcl  42527  lincresunit3lem2  42594  lincresunit3  42595
 Copyright terms: Public domain W3C validator