Theorem syl5eqbr 4688

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

Step	Hyp	Ref	Expression
1		syl5eqbr.2	. 2 |- ( ph -> B R C )
2		syl5eqbr.1	. 2 |- A = B
3		eqid 2622	. 2 |- C = C
4	1, 2, 3	3brtr4g 4687	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  xp1en  8046  map2xp  8130  1sdom  8163  sucxpdom  8169  sniffsupp  8315  wdomima2g  8491  pwsdompw  9026  infunsdom1  9035  infunsdom  9036  infxp  9037  ackbij1lem5  9046  hsmexlem4  9251  imadomg  9356  unidom  9365  unictb  9397  pwcdandom  9489  distrnq  9783  supxrmnf  12147  xov1plusxeqvd  12318  quoremz  12654  quoremnn0ALT  12656  intfrac2  12657  m1modge3gt1  12717  bernneq2  12991  faclbnd4lem1  13080  sqrlem4  13986  reccn2  14327  caucvg  14409  o1fsum  14545  infcvgaux2i  14590  eirrlem  14932  rpnnen2lem12  14954  ruclem12  14970  nno  15098  divalglem5  15120  bitsfzolem  15156  bitsinv1lem  15163  bezoutlem3  15258  lcmfunsnlem  15354  coprmproddvds  15377  oddprmge3  15412  sqnprm  15414  prmreclem6  15625  4sqlem6  15647  4sqlem13  15661  4sqlem16  15664  4sqlem17  15665  2expltfac  15799  odcau  18019  sylow3  18048  efginvrel2  18140  lt6abl  18296  ablfac1lem  18467  evlslem2  19512  gzrngunitlem  19811  zringlpirlem3  19834  znfld  19909  chfacffsupp  20661  cpmidpmatlem3  20677  cctop  20810  csdfil  21698  xpsdsval  22186  nrginvrcnlem  22495  icccmplem2  22626  reconnlem2  22630  iscmet3lem3  23088  minveclem2  23197  minveclem4  23203  ivthlem2  23221  ivthlem3  23222  ovolunlem1a  23264  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovolicc2lem4  23288  unmbl  23305  ioombl1lem4  23329  itg2mono  23520  ibladdlem  23586  iblabsr  23596  iblmulc2  23597  dvferm1lem  23747  dvferm2lem  23749  lhop1lem  23776  dvcvx  23783  ftc1a  23800  plyeq0lem  23966  aannenlem3  24085  geolim3  24094  psercnlem1  24179  pserdvlem2  24182  reeff1olem  24200  pilem2  24206  pilem3  24207  cosq14gt0  24262  cosq14ge0  24263  cosne0  24276  recosf1o  24281  resinf1o  24282  argregt0  24356  logcnlem3  24390  logcnlem4  24391  logf1o2  24396  cxpcn3lem  24488  ang180lem2  24540  acosbnd  24627  atanbndlem  24652  leibpi  24669  cxp2lim  24703  emcllem2  24723  ftalem5  24803  basellem9  24815  vmage0  24847  chpge0  24852  chtub  24937  mersenne  24952  bposlem2  25010  bposlem5  25013  bposlem6  25014  bposlem9  25017  gausslemma2dlem0c  25083  gausslemma2dlem0e  25085  lgseisenlem1  25100  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  mulog2sumlem2  25224  pntpbnd1a  25274  pntibndlem1  25278  pntibndlem3  25281  pntlemc  25284  ostth2  25326  ostth3  25327  pthdlem1  26662  smcnlem  27552  minvecolem2  27731  minvecolem4  27736  strlem5  29114  hstrlem5  29122  abrexdomjm  29345  prct  29492  dya2icoseg  30339  omssubadd  30362  omsmeas  30385  oddpwdc  30416  logdivsqrle  30728  faclim  31632  faclim2  31634  taupilem1  33167  mblfinlem3  33448  mblfinlem4  33449  ibladdnclem  33466  iblmulc2nc  33475  bddiblnc  33480  abrexdom  33525  dalem3  34950  dalem8  34956  dalem25  34984  dalem27  34985  dalem38  34996  dalem44  35002  dalem54  35012  lhpat3  35332  4atexlemunv  35352  4atexlemtlw  35353  4atexlemc  35355  4atexlemnclw  35356  4atexlemex2  35357  4atexlemcnd  35358  cdleme0b  35499  cdleme0c  35500  cdleme0fN  35505  cdlemeulpq  35507  cdleme01N  35508  cdleme0ex1N  35510  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme3g  35521  cdleme3h  35522  cdleme4a  35526  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme9  35540  cdleme11fN  35551  cdleme11k  35555  cdleme15d  35564  cdlemednpq  35586  cdleme19c  35593  cdleme20aN  35597  cdleme20e  35601  cdleme21c  35615  cdleme21ct  35617  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme23a  35637  cdleme28a  35658  cdleme35f  35742  cdlemeg46frv  35813  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg6c  35908  cdlemg31a  35985  cdlemg31b  35986  cdlemk10  36131  cdlemk37  36202  dia2dimlem1  36353  dihjatcclem4  36710  irrapxlem3  37388  pell14qrgapw  37440  dgrsub2  37705  radcnvrat  38513  ressiooinf  39784  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  sumnnodd  39862  climlimsupcex  40001  cnrefiisplem  40055  stoweidlem1  40218  stoweidlem5  40222  stoweidlem7  40224  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem30  40354  fourierdlem42  40366  fourierdlem48  40371  fourierdlem62  40385  fourierdlem63  40386  fourierdlem68  40391  fourierdlem79  40402  sqwvfoura  40445  etransclem32  40483  hoidmvlelem2  40810  iunhoiioolem  40889  vonioolem1  40894  pimdecfgtioo  40927  pimincfltioo  40928  smfmullem1  40998  fmtnoge3  41442  fmtnoprmfac2lem1  41478  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem4a  41525  proththdlem  41530  stgoldbwt  41664  sgoldbeven3prm  41671  mogoldbb  41673  evengpop3  41686  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  lindslinindimp2lem3  42249  fllogbd  42354  nnolog2flm1  42384