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

Theorem syl5eqbr 4056
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 2283 . 2  |-  C  =  C
41, 2, 33brtr4g 4055 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  xp1en  6948  map2xp  7031  1sdom  7065  sucxpdom  7072  wdomima2g  7300  pwsdompw  7830  infunsdom1  7839  infunsdom  7840  infxp  7841  ackbij1lem5  7850  hsmexlem4  8055  imadomg  8159  unidom  8165  unictb  8197  pwcdandom  8289  distrnq  8585  supxrmnf  10636  xov1plusxeqvd  10780  quoremz  10959  quoremnn0ALT  10961  intfrac2  10962  bernneq2  11228  faclbnd4lem1  11306  sqrlem4  11731  reccn2  12070  caucvg  12151  o1fsum  12271  infcvgaux2i  12316  eirrlem  12482  rpnnen2  12504  ruclem12  12519  divalglem5  12596  bitsfzolem  12625  bitsinv1lem  12632  bezoutlem3  12719  sqnprm  12777  prmreclem6  12968  4sqlem6  12990  4sqlem13  13004  4sqlem16  13007  4sqlem17  13008  2expltfac  13105  odcau  14915  sylow3  14944  efginvrel2  15036  lt6abl  15181  ablfac1lem  15303  gzrngunitlem  16436  zlpirlem3  16443  znfld  16514  cctop  16743  csdfil  17589  xpsdsval  17945  nrginvrcnlem  18201  icccmplem2  18328  reconnlem2  18332  iscmet3lem3  18716  minveclem2  18790  minveclem4  18796  ivthlem2  18812  ivthlem3  18813  ovolunlem1a  18855  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovolicc2lem4  18879  unmbl  18895  ioombl1lem4  18918  itg2mono  19108  ibladdlem  19174  iblabsr  19184  iblmulc2  19185  dvferm1lem  19331  dvferm2lem  19333  lhop1lem  19360  dvcvx  19367  ftc1a  19384  plyeq0lem  19592  aannenlem3  19710  geolim3  19719  psercnlem1  19801  pserdvlem2  19804  reeff1olem  19822  pilem2  19828  pilem3  19829  cosq14gt0  19878  cosq14ge0  19879  cosne0  19892  recosf1o  19897  resinf1o  19898  argregt0  19964  logcnlem3  19991  logcnlem4  19992  logf1o2  19997  cxpcn3lem  20087  ang180lem2  20108  acosbnd  20196  atanbndlem  20221  leibpi  20238  cxp2lim  20271  emcllem2  20290  ftalem5  20314  basellem9  20326  vmage0  20359  chpge0  20364  chtub  20451  mersenne  20466  bposlem2  20524  bposlem5  20527  bposlem6  20528  bposlem9  20531  lgseisenlem1  20588  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  mulog2sumlem2  20684  pntpbnd1a  20734  pntibndlem1  20738  pntibndlem3  20741  pntlemc  20744  ostth2  20786  ostth3  20787  smcnlem  21270  minvecolem2  21454  minvecolem4  21459  strlem5  22835  hstrlem5  22843  abrexdomjm  23165  prct  23340  esumpcvgval  23446  toplat  25290  abrexdom  26405  irrapxlem3  26909  pell14qrgapw  26961  dgrsub2  27339  fmul01  27710  stoweidlem1  27750  stoweidlem5  27754  stoweidlem7  27756  wallispi  27819  dalem3  29853  dalem8  29859  dalem25  29887  dalem27  29888  dalem38  29899  dalem44  29905  dalem54  29915  lhpat3  30235  4atexlemunv  30255  4atexlemtlw  30256  4atexlemc  30258  4atexlemnclw  30259  4atexlemex2  30260  4atexlemcnd  30261  cdleme0b  30401  cdleme0c  30402  cdleme0fN  30407  cdlemeulpq  30409  cdleme01N  30410  cdleme0ex1N  30412  cdleme2  30417  cdleme3b  30418  cdleme3c  30419  cdleme3g  30423  cdleme3h  30424  cdleme4a  30428  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme9  30442  cdleme11fN  30453  cdleme11k  30457  cdleme15d  30466  cdlemednpq  30488  cdleme19c  30494  cdleme20aN  30498  cdleme20e  30502  cdleme21c  30516  cdleme21ct  30518  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme23a  30538  cdleme28a  30559  cdleme35f  30643  cdlemeg46frv  30714  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemg2fv2  30789  cdlemg2m  30793  cdlemg6c  30809  cdlemg31a  30886  cdlemg31b  30887  cdlemk10  31032  cdlemk37  31103  dia2dimlem1  31254  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator