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

Theorem syl5eqbr 4248
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 2438 . 2  |-  C  =  C
41, 2, 33brtr4g 4247 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4215
This theorem is referenced by:  xp1en  7197  map2xp  7280  1sdom  7314  sucxpdom  7321  wdomima2g  7557  pwsdompw  8089  infunsdom1  8098  infunsdom  8099  infxp  8100  ackbij1lem5  8109  hsmexlem4  8314  imadomg  8417  unidom  8423  unictb  8455  pwcdandom  8547  distrnq  8843  supxrmnf  10901  xov1plusxeqvd  11046  quoremz  11241  quoremnn0ALT  11243  intfrac2  11244  bernneq2  11511  faclbnd4lem1  11589  sqrlem4  12056  reccn2  12395  caucvg  12477  o1fsum  12597  infcvgaux2i  12642  eirrlem  12808  rpnnen2  12830  ruclem12  12845  divalglem5  12922  bitsfzolem  12951  bitsinv1lem  12958  bezoutlem3  13045  sqnprm  13103  prmreclem6  13294  4sqlem6  13316  4sqlem13  13330  4sqlem16  13333  4sqlem17  13334  2expltfac  13431  odcau  15243  sylow3  15272  efginvrel2  15364  lt6abl  15509  ablfac1lem  15631  gzrngunitlem  16768  zlpirlem3  16775  znfld  16846  cctop  17075  csdfil  17931  xpsdsval  18416  nrginvrcnlem  18731  icccmplem2  18859  reconnlem2  18863  iscmet3lem3  19248  minveclem2  19332  minveclem4  19338  ivthlem2  19354  ivthlem3  19355  ovolunlem1a  19397  ovolfiniun  19402  ovoliunlem3  19405  ovoliun  19406  ovolicc2lem4  19421  unmbl  19437  ioombl1lem4  19460  itg2mono  19648  ibladdlem  19714  iblabsr  19724  iblmulc2  19725  dvferm1lem  19873  dvferm2lem  19875  lhop1lem  19902  dvcvx  19909  ftc1a  19926  plyeq0lem  20134  aannenlem3  20252  geolim3  20261  psercnlem1  20346  pserdvlem2  20349  reeff1olem  20367  pilem2  20373  pilem3  20374  cosq14gt0  20423  cosq14ge0  20424  cosne0  20437  recosf1o  20442  resinf1o  20443  argregt0  20510  logcnlem3  20540  logcnlem4  20541  logf1o2  20546  cxpcn3lem  20636  ang180lem2  20657  acosbnd  20745  atanbndlem  20770  leibpi  20787  cxp2lim  20820  emcllem2  20840  ftalem5  20864  basellem9  20876  vmage0  20909  chpge0  20914  chtub  21001  mersenne  21016  bposlem2  21074  bposlem5  21077  bposlem6  21078  bposlem9  21081  lgseisenlem1  21138  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  chebbnd1lem1  21168  chebbnd1lem2  21169  chebbnd1lem3  21170  mulog2sumlem2  21234  pntpbnd1a  21284  pntibndlem1  21288  pntibndlem3  21291  pntlemc  21294  ostth2  21336  ostth3  21337  smcnlem  22198  minvecolem2  22382  minvecolem4  22387  strlem5  23763  hstrlem5  23771  abrexdomjm  23993  prct  24109  dya2icoseg  24632  faclim  25370  faclim2  25372  mblfinlem3  26257  mblfinlem4  26258  ibladdnclem  26275  iblmulc2nc  26284  bddiblnc  26289  abrexdom  26446  irrapxlem3  26901  pell14qrgapw  26953  dgrsub2  27330  fmul01  27700  fmul01lt1lem1  27704  fmul01lt1lem2  27705  stoweidlem1  27740  stoweidlem5  27744  stoweidlem7  27746  dalem3  30535  dalem8  30541  dalem25  30569  dalem27  30570  dalem38  30581  dalem44  30587  dalem54  30597  lhpat3  30917  4atexlemunv  30937  4atexlemtlw  30938  4atexlemc  30940  4atexlemnclw  30941  4atexlemex2  30942  4atexlemcnd  30943  cdleme0b  31083  cdleme0c  31084  cdleme0fN  31089  cdlemeulpq  31091  cdleme01N  31092  cdleme0ex1N  31094  cdleme2  31099  cdleme3b  31100  cdleme3c  31101  cdleme3g  31105  cdleme3h  31106  cdleme4a  31110  cdleme7aa  31113  cdleme7c  31116  cdleme7d  31117  cdleme7e  31118  cdleme9  31124  cdleme11fN  31135  cdleme11k  31139  cdleme15d  31148  cdlemednpq  31170  cdleme19c  31176  cdleme20aN  31180  cdleme20e  31184  cdleme21c  31198  cdleme21ct  31200  cdleme22e  31215  cdleme22eALTN  31216  cdleme22f  31217  cdleme23a  31220  cdleme28a  31241  cdleme35f  31325  cdlemeg46frv  31396  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemg2fv2  31471  cdlemg2m  31475  cdlemg6c  31491  cdlemg31a  31568  cdlemg31b  31569  cdlemk10  31714  cdlemk37  31785  dia2dimlem1  31936  dihjatcclem4  32293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216
  Copyright terms: Public domain W3C validator