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

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

Proof of Theorem syl5eqbr
StepHypRef Expression
1 syl5eqbr.2 . 2  |-  ( ph  ->  B R C )
2 syl5eqbr.1 . 2  |-  A  =  B
3 eqid 2467 . 2  |-  C  =  C
41, 2, 33brtr4g 4479 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:  xp1en  7600  map2xp  7684  1sdom  7719  sucxpdom  7726  sniffsupp  7865  wdomima2g  8008  pwsdompw  8580  infunsdom1  8589  infunsdom  8590  infxp  8591  ackbij1lem5  8600  hsmexlem4  8805  imadomg  8908  unidom  8914  unictb  8946  pwcdandom  9041  distrnq  9335  supxrmnf  11505  xov1plusxeqvd  11662  quoremz  11946  quoremnn0ALT  11948  intfrac2  11949  bernneq2  12257  faclbnd4lem1  12335  sqrlem4  13038  reccn2  13378  caucvg  13460  o1fsum  13586  infcvgaux2i  13628  eirrlem  13794  rpnnen2  13816  ruclem12  13831  divalglem5  13910  bitsfzolem  13939  bitsinv1lem  13946  bezoutlem3  14033  sqnprm  14094  prmreclem6  14294  4sqlem6  14316  4sqlem13  14330  4sqlem16  14333  4sqlem17  14334  2expltfac  14431  odcau  16420  sylow3  16449  efginvrel2  16541  lt6abl  16688  ablfac1lem  16909  evlslem2  17951  gzrngunitlem  18250  zringlpirlem3  18278  zlpirlem3  18283  znfld  18366  chfacffsupp  19124  cpmidpmatlem3  19140  cctop  19273  csdfil  20130  xpsdsval  20619  nrginvrcnlem  20934  icccmplem2  21063  reconnlem2  21067  iscmet3lem3  21464  minveclem2  21576  minveclem4  21582  ivthlem2  21599  ivthlem3  21600  ovolunlem1a  21642  ovolfiniun  21647  ovoliunlem3  21650  ovoliun  21651  ovolicc2lem4  21666  unmbl  21683  ioombl1lem4  21706  itg2mono  21895  ibladdlem  21961  iblabsr  21971  iblmulc2  21972  dvferm1lem  22120  dvferm2lem  22122  lhop1lem  22149  dvcvx  22156  ftc1a  22173  plyeq0lem  22342  aannenlem3  22460  geolim3  22469  psercnlem1  22554  pserdvlem2  22557  reeff1olem  22575  pilem2  22581  pilem3  22582  cosq14gt0  22636  cosq14ge0  22637  cosne0  22650  recosf1o  22655  resinf1o  22656  argregt0  22723  logcnlem3  22753  logcnlem4  22754  logf1o2  22759  cxpcn3lem  22849  ang180lem2  22870  acosbnd  22959  atanbndlem  22984  leibpi  23001  cxp2lim  23034  emcllem2  23054  ftalem5  23078  basellem9  23090  vmage0  23123  chpge0  23128  chtub  23215  mersenne  23230  bposlem2  23288  bposlem5  23291  bposlem6  23292  bposlem9  23295  lgseisenlem1  23352  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  chebbnd1lem1  23382  chebbnd1lem2  23383  chebbnd1lem3  23384  mulog2sumlem2  23448  pntpbnd1a  23498  pntibndlem1  23502  pntibndlem3  23505  pntlemc  23508  ostth2  23550  ostth3  23551  smcnlem  25283  minvecolem2  25467  minvecolem4  25472  strlem5  26850  hstrlem5  26858  abrexdomjm  27079  prct  27207  dya2icoseg  27888  oddpwdc  27933  faclim  28748  faclim2  28750  mblfinlem3  29630  mblfinlem4  29631  ibladdnclem  29648  iblmulc2nc  29657  bddiblnc  29662  abrexdom  29824  irrapxlem3  30364  pell14qrgapw  30416  dgrsub2  30688  fmul01  31130  fmul01lt1lem1  31134  fmul01lt1lem2  31135  stoweidlem1  31301  stoweidlem5  31305  stoweidlem7  31307  dirkercncflem1  31403  fourierdlem63  31470  lindslinindimp2lem3  32134  dalem3  34460  dalem8  34466  dalem25  34494  dalem27  34495  dalem38  34506  dalem44  34512  dalem54  34522  lhpat3  34842  4atexlemunv  34862  4atexlemtlw  34863  4atexlemc  34865  4atexlemnclw  34866  4atexlemex2  34867  4atexlemcnd  34868  cdleme0b  35008  cdleme0c  35009  cdleme0fN  35014  cdlemeulpq  35016  cdleme01N  35017  cdleme0ex1N  35019  cdleme2  35024  cdleme3b  35025  cdleme3c  35026  cdleme3g  35030  cdleme3h  35031  cdleme4a  35035  cdleme7aa  35038  cdleme7c  35041  cdleme7d  35042  cdleme7e  35043  cdleme9  35049  cdleme11fN  35060  cdleme11k  35064  cdleme15d  35073  cdlemednpq  35095  cdleme19c  35101  cdleme20aN  35105  cdleme20e  35109  cdleme21c  35123  cdleme21ct  35125  cdleme22e  35140  cdleme22eALTN  35141  cdleme22f  35142  cdleme23a  35145  cdleme28a  35166  cdleme35f  35250  cdlemeg46frv  35321  cdlemeg46rgv  35324  cdlemeg46req  35325  cdlemg2fv2  35396  cdlemg2m  35400  cdlemg6c  35416  cdlemg31a  35493  cdlemg31b  35494  cdlemk10  35639  cdlemk37  35710  dia2dimlem1  35861  dihjatcclem4  36218  taupilem1  36767
  Copyright terms: Public domain W3C validator