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

Theorem syl5eqbr 4432
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 2454 . 2  |-  C  =  C
41, 2, 33brtr4g 4431 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   class class class wbr 4399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400
This theorem is referenced by:  xp1en  7506  map2xp  7590  1sdom  7625  sucxpdom  7632  sniffsupp  7769  wdomima2g  7911  pwsdompw  8483  infunsdom1  8492  infunsdom  8493  infxp  8494  ackbij1lem5  8503  hsmexlem4  8708  imadomg  8811  unidom  8817  unictb  8849  pwcdandom  8944  distrnq  9240  supxrmnf  11390  xov1plusxeqvd  11547  quoremz  11810  quoremnn0ALT  11812  intfrac2  11813  bernneq2  12107  faclbnd4lem1  12185  sqrlem4  12852  reccn2  13191  caucvg  13273  o1fsum  13393  infcvgaux2i  13437  eirrlem  13603  rpnnen2  13625  ruclem12  13640  divalglem5  13718  bitsfzolem  13747  bitsinv1lem  13754  bezoutlem3  13841  sqnprm  13901  prmreclem6  14099  4sqlem6  14121  4sqlem13  14135  4sqlem16  14138  4sqlem17  14139  2expltfac  14236  odcau  16223  sylow3  16252  efginvrel2  16344  lt6abl  16491  ablfac1lem  16690  evlslem2  17720  gzrngunitlem  18001  zringlpirlem3  18029  zlpirlem3  18034  znfld  18117  cctop  18741  csdfil  19598  xpsdsval  20087  nrginvrcnlem  20402  icccmplem2  20531  reconnlem2  20535  iscmet3lem3  20932  minveclem2  21044  minveclem4  21050  ivthlem2  21067  ivthlem3  21068  ovolunlem1a  21110  ovolfiniun  21115  ovoliunlem3  21118  ovoliun  21119  ovolicc2lem4  21134  unmbl  21151  ioombl1lem4  21174  itg2mono  21363  ibladdlem  21429  iblabsr  21439  iblmulc2  21440  dvferm1lem  21588  dvferm2lem  21590  lhop1lem  21617  dvcvx  21624  ftc1a  21641  plyeq0lem  21810  aannenlem3  21928  geolim3  21937  psercnlem1  22022  pserdvlem2  22025  reeff1olem  22043  pilem2  22049  pilem3  22050  cosq14gt0  22104  cosq14ge0  22105  cosne0  22118  recosf1o  22123  resinf1o  22124  argregt0  22191  logcnlem3  22221  logcnlem4  22222  logf1o2  22227  cxpcn3lem  22317  ang180lem2  22338  acosbnd  22427  atanbndlem  22452  leibpi  22469  cxp2lim  22502  emcllem2  22522  ftalem5  22546  basellem9  22558  vmage0  22591  chpge0  22596  chtub  22683  mersenne  22698  bposlem2  22756  bposlem5  22759  bposlem6  22760  bposlem9  22763  lgseisenlem1  22820  lgsquadlem1  22825  lgsquadlem2  22826  lgsquadlem3  22827  chebbnd1lem1  22850  chebbnd1lem2  22851  chebbnd1lem3  22852  mulog2sumlem2  22916  pntpbnd1a  22966  pntibndlem1  22970  pntibndlem3  22973  pntlemc  22976  ostth2  23018  ostth3  23019  smcnlem  24243  minvecolem2  24427  minvecolem4  24432  strlem5  25810  hstrlem5  25818  abrexdomjm  26039  prct  26162  dya2icoseg  26835  oddpwdc  26880  faclim  27695  faclim2  27697  mblfinlem3  28577  mblfinlem4  28578  ibladdnclem  28595  iblmulc2nc  28604  bddiblnc  28609  abrexdom  28771  irrapxlem3  29312  pell14qrgapw  29364  dgrsub2  29638  fmul01  29908  fmul01lt1lem1  29912  fmul01lt1lem2  29913  stoweidlem1  29943  stoweidlem5  29947  stoweidlem7  29949  lindslinindimp2lem3  31112  chfacffsupp  31327  cpmidpmatlem3  31343  dalem3  33631  dalem8  33637  dalem25  33665  dalem27  33666  dalem38  33677  dalem44  33683  dalem54  33693  lhpat3  34013  4atexlemunv  34033  4atexlemtlw  34034  4atexlemc  34036  4atexlemnclw  34037  4atexlemex2  34038  4atexlemcnd  34039  cdleme0b  34179  cdleme0c  34180  cdleme0fN  34185  cdlemeulpq  34187  cdleme01N  34188  cdleme0ex1N  34190  cdleme2  34195  cdleme3b  34196  cdleme3c  34197  cdleme3g  34201  cdleme3h  34202  cdleme4a  34206  cdleme7aa  34209  cdleme7c  34212  cdleme7d  34213  cdleme7e  34214  cdleme9  34220  cdleme11fN  34231  cdleme11k  34235  cdleme15d  34244  cdlemednpq  34266  cdleme19c  34272  cdleme20aN  34276  cdleme20e  34280  cdleme21c  34294  cdleme21ct  34296  cdleme22e  34311  cdleme22eALTN  34312  cdleme22f  34313  cdleme23a  34316  cdleme28a  34337  cdleme35f  34421  cdlemeg46frv  34492  cdlemeg46rgv  34495  cdlemeg46req  34496  cdlemg2fv2  34567  cdlemg2m  34571  cdlemg6c  34587  cdlemg31a  34664  cdlemg31b  34665  cdlemk10  34810  cdlemk37  34881  dia2dimlem1  35032  dihjatcclem4  35389  taupilem1  35938
  Copyright terms: Public domain W3C validator