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

Theorem syl5eqbr 4072
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 2296 . 2  |-  C  =  C
41, 2, 33brtr4g 4071 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  xp1en  6964  map2xp  7047  1sdom  7081  sucxpdom  7088  wdomima2g  7316  pwsdompw  7846  infunsdom1  7855  infunsdom  7856  infxp  7857  ackbij1lem5  7866  hsmexlem4  8071  imadomg  8175  unidom  8181  unictb  8213  pwcdandom  8305  distrnq  8601  supxrmnf  10652  xov1plusxeqvd  10796  quoremz  10975  quoremnn0ALT  10977  intfrac2  10978  bernneq2  11244  faclbnd4lem1  11322  sqrlem4  11747  reccn2  12086  caucvg  12167  o1fsum  12287  infcvgaux2i  12332  eirrlem  12498  rpnnen2  12520  ruclem12  12535  divalglem5  12612  bitsfzolem  12641  bitsinv1lem  12648  bezoutlem3  12735  sqnprm  12793  prmreclem6  12984  4sqlem6  13006  4sqlem13  13020  4sqlem16  13023  4sqlem17  13024  2expltfac  13121  odcau  14931  sylow3  14960  efginvrel2  15052  lt6abl  15197  ablfac1lem  15319  gzrngunitlem  16452  zlpirlem3  16459  znfld  16530  cctop  16759  csdfil  17605  xpsdsval  17961  nrginvrcnlem  18217  icccmplem2  18344  reconnlem2  18348  iscmet3lem3  18732  minveclem2  18806  minveclem4  18812  ivthlem2  18828  ivthlem3  18829  ovolunlem1a  18871  ovolfiniun  18876  ovoliunlem3  18879  ovoliun  18880  ovolicc2lem4  18895  unmbl  18911  ioombl1lem4  18934  itg2mono  19124  ibladdlem  19190  iblabsr  19200  iblmulc2  19201  dvferm1lem  19347  dvferm2lem  19349  lhop1lem  19376  dvcvx  19383  ftc1a  19400  plyeq0lem  19608  aannenlem3  19726  geolim3  19735  psercnlem1  19817  pserdvlem2  19820  reeff1olem  19838  pilem2  19844  pilem3  19845  cosq14gt0  19894  cosq14ge0  19895  cosne0  19908  recosf1o  19913  resinf1o  19914  argregt0  19980  logcnlem3  20007  logcnlem4  20008  logf1o2  20013  cxpcn3lem  20103  ang180lem2  20124  acosbnd  20212  atanbndlem  20237  leibpi  20254  cxp2lim  20287  emcllem2  20306  ftalem5  20330  basellem9  20342  vmage0  20375  chpge0  20380  chtub  20467  mersenne  20482  bposlem2  20540  bposlem5  20543  bposlem6  20544  bposlem9  20547  lgseisenlem1  20604  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1lem3  20636  mulog2sumlem2  20700  pntpbnd1a  20750  pntibndlem1  20754  pntibndlem3  20757  pntlemc  20760  ostth2  20802  ostth3  20803  smcnlem  21286  minvecolem2  21470  minvecolem4  21475  strlem5  22851  hstrlem5  22859  abrexdomjm  23181  prct  23355  esumpcvgval  23461  faclim  24126  ibladdnclem  25007  iblmulc2nc  25016  bddiblnc  25021  toplat  25393  abrexdom  26508  irrapxlem3  27012  pell14qrgapw  27064  dgrsub2  27442  fmul01  27813  stoweidlem1  27853  stoweidlem5  27857  stoweidlem7  27859  wallispi  27922  dalem3  30475  dalem8  30481  dalem25  30509  dalem27  30510  dalem38  30521  dalem44  30527  dalem54  30537  lhpat3  30857  4atexlemunv  30877  4atexlemtlw  30878  4atexlemc  30880  4atexlemnclw  30881  4atexlemex2  30882  4atexlemcnd  30883  cdleme0b  31023  cdleme0c  31024  cdleme0fN  31029  cdlemeulpq  31031  cdleme01N  31032  cdleme0ex1N  31034  cdleme2  31039  cdleme3b  31040  cdleme3c  31041  cdleme3g  31045  cdleme3h  31046  cdleme4a  31050  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme9  31064  cdleme11fN  31075  cdleme11k  31079  cdleme15d  31088  cdlemednpq  31110  cdleme19c  31116  cdleme20aN  31120  cdleme20e  31124  cdleme21c  31138  cdleme21ct  31140  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme23a  31160  cdleme28a  31181  cdleme35f  31265  cdlemeg46frv  31336  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemg2fv2  31411  cdlemg2m  31415  cdlemg6c  31431  cdlemg31a  31508  cdlemg31b  31509  cdlemk10  31654  cdlemk37  31725  dia2dimlem1  31876  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator