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

Theorem syl6breq 4486
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 2467 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4478 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  syl6breqr  4487  difsnen  7596  marypha1lem  7889  en2eleq  8382  en2other2  8383  cda0en  8555  ackbij1lem5  8600  alephadd  8948  prlem934  9407  ltexprlem2  9411  recgt0ii  10447  discr  12267  faclbnd4lem1  12335  hashfun  12457  sqrlem7  13041  resqrex  13043  abs3lemi  13201  supcvg  13626  ege2le3  13683  cos01gt0  13783  sin02gt0  13784  bitsfzolem  13939  bitsmod  13941  prmreclem2  14290  f1otrspeq  16268  pmtrf  16276  pmtrmvd  16277  pmtrfinv  16282  efgi0  16534  efgi1  16535  dprdf1  16870  metustexhalfOLD  20801  metustexhalf  20802  nlmvscnlem2  20929  icccmplem2  21063  xrge0tsms  21074  iimulcl  21172  pcoass  21259  ipcnlem2  21419  ivthlem3  21600  vitalilem4  21755  vitali  21757  dvef  22116  ply1rem  22299  aaliou3lem2  22473  abelthlem8  22568  abelthlem9  22569  cosne0  22650  sinord  22654  tanregt0  22659  argimgt0  22725  logf1o2  22759  logtayllem  22768  cxpcn3lem  22849  ang180lem2  22870  ang180lem3  22871  atanlogsublem  22974  bndatandm  22988  leibpi  23001  emcllem6  23058  emcllem7  23059  ftalem5  23078  basellem7  23088  basellem9  23090  ppieq0  23178  ppiub  23207  chpeq0  23211  chpub  23223  logfacrlim  23227  logexprlim  23228  bposlem1  23287  bposlem2  23288  lgslem3  23301  lgsquadlem1  23357  lgsquadlem3  23359  chebbnd1lem3  23384  chtppilim  23388  chpchtlim  23392  dchrvmasumiflem1  23414  dchrisum0re  23426  mudivsum  23443  mulog2sumlem2  23448  pntibndlem2  23504  pntlemb  23510  pntlemh  23512  ostth3  23551  norm3lem  25742  nmopadjlem  26684  nmopcoadji  26696  hstle  26825  stadd3i  26843  strlem5  26850  gsumle  27433  xrge0iifcnv  27551  eulerpartlems  27939  signsply0  28148  signsvtp  28180  lgamgulmlem5  28215  lgamcvg2  28237  sinccvglem  28513  faclim2  28750  ismblfin  29632  irrapxlem2  30363  pellexlem2  30370  areaquad  30789  fmul01  31130  clim1fr1  31143  stoweidlem14  31314  stoweidlem16  31316  stoweidlem26  31326  stoweidlem41  31341  stoweidlem42  31342  stoweidlem45  31345  wallispi  31370  stirlinglem1  31374  fourierdlem42  31449  fourierdlem47  31454  fourierdlem63  31470  fouriersw  31532  lincfsuppcl  32087  lincresunit3lem2  32154  lincresunit3  32155
  Copyright terms: Public domain W3C validator