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

Theorem syl5eqbr 4245
Description: B 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 2436 . 2  |-  C  =  C
41, 2, 33brtr4g 4244 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  xp1en  7194  map2xp  7277  1sdom  7311  sucxpdom  7318  wdomima2g  7554  pwsdompw  8084  infunsdom1  8093  infunsdom  8094  infxp  8095  ackbij1lem5  8104  hsmexlem4  8309  imadomg  8412  unidom  8418  unictb  8450  pwcdandom  8542  distrnq  8838  supxrmnf  10896  xov1plusxeqvd  11041  quoremz  11236  quoremnn0ALT  11238  intfrac2  11239  bernneq2  11506  faclbnd4lem1  11584  sqrlem4  12051  reccn2  12390  caucvg  12472  o1fsum  12592  infcvgaux2i  12637  eirrlem  12803  rpnnen2  12825  ruclem12  12840  divalglem5  12917  bitsfzolem  12946  bitsinv1lem  12953  bezoutlem3  13040  sqnprm  13098  prmreclem6  13289  4sqlem6  13311  4sqlem13  13325  4sqlem16  13328  4sqlem17  13329  2expltfac  13426  odcau  15238  sylow3  15267  efginvrel2  15359  lt6abl  15504  ablfac1lem  15626  gzrngunitlem  16763  zlpirlem3  16770  znfld  16841  cctop  17070  csdfil  17926  xpsdsval  18411  nrginvrcnlem  18726  icccmplem2  18854  reconnlem2  18858  iscmet3lem3  19243  minveclem2  19327  minveclem4  19333  ivthlem2  19349  ivthlem3  19350  ovolunlem1a  19392  ovolfiniun  19397  ovoliunlem3  19400  ovoliun  19401  ovolicc2lem4  19416  unmbl  19432  ioombl1lem4  19455  itg2mono  19645  ibladdlem  19711  iblabsr  19721  iblmulc2  19722  dvferm1lem  19868  dvferm2lem  19870  lhop1lem  19897  dvcvx  19904  ftc1a  19921  plyeq0lem  20129  aannenlem3  20247  geolim3  20256  psercnlem1  20341  pserdvlem2  20344  reeff1olem  20362  pilem2  20368  pilem3  20369  cosq14gt0  20418  cosq14ge0  20419  cosne0  20432  recosf1o  20437  resinf1o  20438  argregt0  20505  logcnlem3  20535  logcnlem4  20536  logf1o2  20541  cxpcn3lem  20631  ang180lem2  20652  acosbnd  20740  atanbndlem  20765  leibpi  20782  cxp2lim  20815  emcllem2  20835  ftalem5  20859  basellem9  20871  vmage0  20904  chpge0  20909  chtub  20996  mersenne  21011  bposlem2  21069  bposlem5  21072  bposlem6  21073  bposlem9  21076  lgseisenlem1  21133  lgsquadlem1  21138  lgsquadlem2  21139  lgsquadlem3  21140  chebbnd1lem1  21163  chebbnd1lem2  21164  chebbnd1lem3  21165  mulog2sumlem2  21229  pntpbnd1a  21279  pntibndlem1  21283  pntibndlem3  21286  pntlemc  21289  ostth2  21331  ostth3  21332  smcnlem  22193  minvecolem2  22377  minvecolem4  22382  strlem5  23758  hstrlem5  23766  abrexdomjm  23988  prct  24104  dya2icoseg  24627  faclim  25365  faclim2  25367  mblfinlem3  26245  mblfinlem4  26246  ibladdnclem  26261  iblmulc2nc  26270  bddiblnc  26275  abrexdom  26432  irrapxlem3  26887  pell14qrgapw  26939  dgrsub2  27316  fmul01  27686  fmul01lt1lem1  27690  fmul01lt1lem2  27691  stoweidlem1  27726  stoweidlem5  27730  stoweidlem7  27732  dalem3  30461  dalem8  30467  dalem25  30495  dalem27  30496  dalem38  30507  dalem44  30513  dalem54  30523  lhpat3  30843  4atexlemunv  30863  4atexlemtlw  30864  4atexlemc  30866  4atexlemnclw  30867  4atexlemex2  30868  4atexlemcnd  30869  cdleme0b  31009  cdleme0c  31010  cdleme0fN  31015  cdlemeulpq  31017  cdleme01N  31018  cdleme0ex1N  31020  cdleme2  31025  cdleme3b  31026  cdleme3c  31027  cdleme3g  31031  cdleme3h  31032  cdleme4a  31036  cdleme7aa  31039  cdleme7c  31042  cdleme7d  31043  cdleme7e  31044  cdleme9  31050  cdleme11fN  31061  cdleme11k  31065  cdleme15d  31074  cdlemednpq  31096  cdleme19c  31102  cdleme20aN  31106  cdleme20e  31110  cdleme21c  31124  cdleme21ct  31126  cdleme22e  31141  cdleme22eALTN  31142  cdleme22f  31143  cdleme23a  31146  cdleme28a  31167  cdleme35f  31251  cdlemeg46frv  31322  cdlemeg46rgv  31325  cdlemeg46req  31326  cdlemg2fv2  31397  cdlemg2m  31401  cdlemg6c  31417  cdlemg31a  31494  cdlemg31b  31495  cdlemk10  31640  cdlemk37  31711  dia2dimlem1  31862  dihjatcclem4  32219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator