Theorem syl5eqbr 4965

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
syl5eqbr.1	⊢ 𝐴 = 𝐵
syl5eqbr.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
syl5eqbr	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl5eqbr

Step	Hyp	Ref	Expression
1		syl5eqbr.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		syl5eqbr.1	. 2 ⊢ 𝐴 = 𝐵
3		eqid 2778	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr4g 4964	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1507   class class class wbr 4930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-br 4931

This theorem is referenced by:  map1  8391  xp1en  8401  map2xp  8485  1sdom  8518  sucxpdom  8524  sniffsupp  8670  wdomima2g  8847  endjudisj  9394  dju1dif  9398  mapdjuen  9406  djuxpdom  9411  djufi  9412  pwsdompw  9426  infunsdom1  9435  infunsdom  9436  infxp  9437  ackbij1lem5  9446  hsmexlem4  9651  imadomg  9756  unidom  9765  unictb  9797  pwxpndom2  9887  pwdjundom  9889  distrnq  10183  nnne0  11477  supxrmnf  12529  xov1plusxeqvd  12703  quoremz  13041  quoremnn0ALT  13043  intfrac2  13044  m1modge3gt1  13104  bernneq2  13409  faclbnd4lem1  13471  sqrlem4  14469  reccn2  14817  caucvg  14899  o1fsum  15031  infcvgaux2i  15076  eirrlem  15420  rpnnen2lem12  15441  ruclem12  15457  nno  15596  divalglem5  15611  bitsfzolem  15646  bitsinv1lem  15653  bezoutlem3  15748  lcmfunsnlem  15844  coprmproddvds  15866  oddprmge3  15903  ge2nprmge4  15904  sqnprm  15905  prmreclem6  16116  4sqlem6  16138  4sqlem13  16152  4sqlem16  16155  4sqlem17  16156  2expltfac  16285  odcau  18493  sylow3  18522  efginvrel2  18614  lt6abl  18772  ablfac1lem  18943  evlslem2  20008  gzrngunitlem  20315  zringlpirlem3  20338  znfld  20412  chfacffsupp  21171  cpmidpmatlem3  21187  cctop  21321  csdfil  22209  xpsdsval  22697  nrginvrcnlem  23006  icccmplem2  23137  reconnlem2  23141  iscmet3lem3  23599  minveclem2  23735  minveclem4  23741  ivthlem2  23759  ivthlem3  23760  ovolunlem1a  23803  ovolfiniun  23808  ovoliunlem3  23811  ovoliun  23812  ovolicc2lem4  23827  unmbl  23844  ioombl1lem4  23868  itg2mono  24060  ibladdlem  24126  iblabsr  24136  iblmulc2  24137  dvferm1lem  24287  dvferm2lem  24289  lhop1lem  24316  dvcvx  24323  ftc1a  24340  plyeq0lem  24506  aannenlem3  24625  geolim3  24634  psercnlem1  24719  pserdvlem2  24722  reeff1olem  24740  pilem2  24746  pilem3  24747  cosq14gt0  24802  cosq14ge0  24803  cosne0  24818  recosf1o  24823  resinf1o  24824  argregt0  24897  logcnlem3  24931  logcnlem4  24932  logf1o2  24937  cxpcn3lem  25032  ang180lem2  25092  acosbnd  25182  atanbndlem  25207  leibpi  25225  cxp2lim  25259  emcllem2  25279  ftalem5  25359  basellem9  25371  vmage0  25403  chpge0  25408  chtub  25493  mersenne  25508  bposlem2  25566  bposlem5  25569  bposlem6  25570  bposlem9  25573  gausslemma2dlem0c  25639  gausslemma2dlem0e  25641  lgseisenlem1  25656  lgsquadlem1  25661  lgsquadlem2  25662  lgsquadlem3  25663  chebbnd1lem1  25750  chebbnd1lem2  25751  chebbnd1lem3  25752  mulog2sumlem2  25816  pntpbnd1a  25866  pntibndlem1  25870  pntibndlem3  25873  pntlemc  25876  ostth2  25918  ostth3  25919  pthdlem1  27258  numclwlk1lem2  27926  smcnlem  28254  minvecolem2  28433  minvecolem4  28438  strlem5  29816  hstrlem5  29824  abrexdomjm  30049  prct  30205  dvdschrmulg  30537  dya2icoseg  31180  omssubadd  31203  omsmeas  31226  oddpwdc  31257  logdivsqrle  31569  faclim  32498  faclim2  32500  taupilem1  34044  mblfinlem3  34372  mblfinlem4  34373  ibladdnclem  34389  iblmulc2nc  34398  bddiblnc  34403  abrexdom  34447  dalem3  36245  dalem8  36251  dalem25  36279  dalem27  36280  dalem38  36291  dalem44  36297  dalem54  36307  lhpat3  36627  4atexlemunv  36647  4atexlemtlw  36648  4atexlemc  36650  4atexlemnclw  36651  4atexlemex2  36652  4atexlemcnd  36653  cdleme0b  36793  cdleme0c  36794  cdleme0fN  36799  cdlemeulpq  36801  cdleme01N  36802  cdleme0ex1N  36804  cdleme2  36809  cdleme3b  36810  cdleme3c  36811  cdleme3g  36815  cdleme3h  36816  cdleme4a  36820  cdleme7aa  36823  cdleme7c  36826  cdleme7d  36827  cdleme7e  36828  cdleme9  36834  cdleme11fN  36845  cdleme11k  36849  cdleme15d  36858  cdlemednpq  36880  cdleme19c  36886  cdleme20aN  36890  cdleme20e  36894  cdleme21c  36908  cdleme21ct  36910  cdleme22e  36925  cdleme22eALTN  36926  cdleme22f  36927  cdleme23a  36930  cdleme28a  36951  cdleme35f  37035  cdlemeg46frv  37106  cdlemeg46rgv  37109  cdlemeg46req  37110  cdlemg2fv2  37181  cdlemg2m  37185  cdlemg6c  37201  cdlemg31a  37278  cdlemg31b  37279  cdlemk10  37424  cdlemk37  37495  dia2dimlem1  37645  dihjatcclem4  38002  irrapxlem3  38817  pell14qrgapw  38869  dgrsub2  39131  radcnvrat  40062  ressiooinf  41265  fmul01  41293  fmul01lt1lem1  41297  fmul01lt1lem2  41298  sumnnodd  41343  climlimsupcex  41482  cnrefiisplem  41542  stoweidlem1  41718  stoweidlem5  41722  stoweidlem7  41724  dirkercncflem1  41820  dirkercncflem4  41823  fourierdlem30  41854  fourierdlem42  41866  fourierdlem48  41871  fourierdlem62  41885  fourierdlem63  41886  fourierdlem68  41891  fourierdlem79  41902  sqwvfoura  41945  etransclem32  41983  hoidmvlelem2  42310  iunhoiioolem  42389  vonioolem1  42394  pimdecfgtioo  42427  pimincfltioo  42428  smfmullem1  42498  fmtnoge3  43061  fmtnoprmfac2lem1  43097  sfprmdvdsmersenne  43137  lighneallem2  43140  lighneallem4a  43142  proththdlem  43147  stgoldbwt  43310  sgoldbeven3prm  43317  mogoldbb  43319  evengpop3  43332  bgoldbtbndlem2  43340  bgoldbtbndlem3  43341  lindslinindimp2lem3  43883  fllogbd  43989  nnolog2flm1  44019