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

Theorem syl6breq 4336
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl6breq.1  |-  ( ph  ->  A R B )
syl6breq.2  |-  B  =  C
Assertion
Ref Expression
syl6breq  |-  ( ph  ->  A R C )

Proof of Theorem syl6breq
StepHypRef Expression
1 syl6breq.1 . 2  |-  ( ph  ->  A R B )
2 eqid 2443 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4328 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   class class class wbr 4297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298
This theorem is referenced by:  syl6breqr  4337  difsnen  7398  marypha1lem  7688  en2eleq  8180  en2other2  8181  cda0en  8353  ackbij1lem5  8398  alephadd  8746  prlem934  9207  ltexprlem2  9211  recgt0ii  10243  discr  12006  faclbnd4lem1  12074  hashfun  12204  sqrlem7  12743  resqrex  12745  abs3lemi  12902  supcvg  13323  ege2le3  13380  cos01gt0  13480  sin02gt0  13481  bitsfzolem  13635  bitsmod  13637  prmreclem2  13983  f1otrspeq  15958  pmtrf  15966  pmtrmvd  15967  pmtrfinv  15972  efgi0  16222  efgi1  16223  dprdf1  16535  metustexhalfOLD  20143  metustexhalf  20144  nlmvscnlem2  20271  icccmplem2  20405  xrge0tsms  20416  iimulcl  20514  pcoass  20601  ipcnlem2  20761  ivthlem3  20942  vitalilem4  21096  vitali  21098  dvef  21457  ply1rem  21640  aaliou3lem2  21814  abelthlem8  21909  abelthlem9  21910  cosne0  21991  sinord  21995  tanregt0  22000  argimgt0  22066  logf1o2  22100  logtayllem  22109  cxpcn3lem  22190  ang180lem2  22211  ang180lem3  22212  atanlogsublem  22315  bndatandm  22329  leibpi  22342  emcllem6  22399  emcllem7  22400  ftalem5  22419  basellem7  22429  basellem9  22431  ppieq0  22519  ppiub  22548  chpeq0  22552  chpub  22564  logfacrlim  22568  logexprlim  22569  bposlem1  22628  bposlem2  22629  lgslem3  22642  lgsquadlem1  22698  lgsquadlem3  22700  chebbnd1lem3  22725  chtppilim  22729  chpchtlim  22733  dchrvmasumiflem1  22755  dchrisum0re  22767  mudivsum  22784  mulog2sumlem2  22789  pntibndlem2  22845  pntlemb  22851  pntlemh  22853  ostth3  22892  norm3lem  24556  nmopadjlem  25498  nmopcoadji  25510  hstle  25639  stadd3i  25657  strlem5  25664  xrge0iifcnv  26368  eulerpartlems  26748  signsply0  26957  signsvtp  26989  lgamgulmlem5  27024  lgamcvg2  27046  sinccvglem  27322  faclim2  27559  ismblfin  28437  irrapxlem2  29169  pellexlem2  29176  areaquad  29597  fmul01  29766  clim1fr1  29779  stoweidlem14  29814  stoweidlem16  29816  stoweidlem26  29826  stoweidlem41  29841  stoweidlem42  29842  stoweidlem45  29845  wallispi  29870  stirlinglem1  29874  lincfsuppcl  30952  lincresunit3lem2  31019  lincresunit3  31020
  Copyright terms: Public domain W3C validator