Theorem syl5eqbr 4618

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 2610	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr4g 4617	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  xp1en  7931  map2xp  8015  1sdom  8048  sucxpdom  8054  sniffsupp  8198  wdomima2g  8374  pwsdompw  8909  infunsdom1  8918  infunsdom  8919  infxp  8920  ackbij1lem5  8929  hsmexlem4  9134  imadomg  9237  unidom  9244  unictb  9276  pwcdandom  9368  distrnq  9662  supxrmnf  12019  xov1plusxeqvd  12189  quoremz  12516  quoremnn0ALT  12518  intfrac2  12519  m1modge3gt1  12579  bernneq2  12853  faclbnd4lem1  12942  sqrlem4  13834  reccn2  14175  caucvg  14257  o1fsum  14386  infcvgaux2i  14429  eirrlem  14771  rpnnen2lem12  14793  ruclem12  14809  nno  14936  divalglem5  14958  bitsfzolem  14994  bitsinv1lem  15001  bezoutlem3  15096  lcmfunsnlem  15192  coprmproddvds  15215  oddprmge3  15250  sqnprm  15252  prmreclem6  15463  4sqlem6  15485  4sqlem13  15499  4sqlem16  15502  4sqlem17  15503  2expltfac  15637  odcau  17842  sylow3  17871  efginvrel2  17963  lt6abl  18119  ablfac1lem  18290  evlslem2  19333  gzrngunitlem  19630  zringlpirlem3  19653  znfld  19728  chfacffsupp  20480  cpmidpmatlem3  20496  cctop  20620  csdfil  21508  xpsdsval  21996  nrginvrcnlem  22305  icccmplem2  22434  reconnlem2  22438  iscmet3lem3  22896  minveclem2  23005  minveclem4  23011  ivthlem2  23028  ivthlem3  23029  ovolunlem1a  23071  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovolicc2lem4  23095  unmbl  23112  ioombl1lem4  23136  itg2mono  23326  ibladdlem  23392  iblabsr  23402  iblmulc2  23403  dvferm1lem  23551  dvferm2lem  23553  lhop1lem  23580  dvcvx  23587  ftc1a  23604  plyeq0lem  23770  aannenlem3  23889  geolim3  23898  psercnlem1  23983  pserdvlem2  23986  reeff1olem  24004  pilem2  24010  pilem3  24011  cosq14gt0  24066  cosq14ge0  24067  cosne0  24080  recosf1o  24085  resinf1o  24086  argregt0  24160  logcnlem3  24190  logcnlem4  24191  logf1o2  24196  cxpcn3lem  24288  ang180lem2  24340  acosbnd  24427  atanbndlem  24452  leibpi  24469  cxp2lim  24503  emcllem2  24523  ftalem5  24603  basellem9  24615  vmage0  24647  chpge0  24652  chtub  24737  mersenne  24752  bposlem2  24810  bposlem5  24813  bposlem6  24814  bposlem9  24817  gausslemma2dlem0c  24883  gausslemma2dlem0e  24885  lgseisenlem1  24900  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  mulog2sumlem2  25024  pntpbnd1a  25074  pntibndlem1  25078  pntibndlem3  25081  pntlemc  25084  ostth2  25126  ostth3  25127  smcnlem  26936  minvecolem2  27115  minvecolem4  27120  strlem5  28498  hstrlem5  28506  abrexdomjm  28729  prct  28875  dya2icoseg  29666  omssubadd  29689  omsmeas  29712  oddpwdc  29743  faclim  30885  faclim2  30887  taupilem1  32344  mblfinlem3  32618  mblfinlem4  32619  ibladdnclem  32636  iblmulc2nc  32645  bddiblnc  32650  abrexdom  32695  dalem3  33968  dalem8  33974  dalem25  34002  dalem27  34003  dalem38  34014  dalem44  34020  dalem54  34030  lhpat3  34350  4atexlemunv  34370  4atexlemtlw  34371  4atexlemc  34373  4atexlemnclw  34374  4atexlemex2  34375  4atexlemcnd  34376  cdleme0b  34517  cdleme0c  34518  cdleme0fN  34523  cdlemeulpq  34525  cdleme01N  34526  cdleme0ex1N  34528  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3g  34539  cdleme3h  34540  cdleme4a  34544  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme9  34558  cdleme11fN  34569  cdleme11k  34573  cdleme15d  34582  cdlemednpq  34604  cdleme19c  34611  cdleme20aN  34615  cdleme20e  34619  cdleme21c  34633  cdleme21ct  34635  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme23a  34655  cdleme28a  34676  cdleme35f  34760  cdlemeg46frv  34831  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg6c  34926  cdlemg31a  35003  cdlemg31b  35004  cdlemk10  35149  cdlemk37  35220  dia2dimlem1  35371  dihjatcclem4  35728  irrapxlem3  36406  pell14qrgapw  36458  dgrsub2  36724  radcnvrat  37535  ressiooinf  38631  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  sumnnodd  38697  stoweidlem1  38894  stoweidlem5  38898  stoweidlem7  38900  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem30  39030  fourierdlem42  39042  fourierdlem48  39047  fourierdlem62  39061  fourierdlem63  39062  fourierdlem68  39067  fourierdlem79  39078  sqwvfoura  39121  etransclem32  39159  hoidmvlelem2  39486  iunhoiioolem  39566  vonioolem1  39571  pimdecfgtioo  39604  pimincfltioo  39605  smfmullem1  39676  fmtnoge3  39980  fmtnoprmfac2lem1  40016  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem4a  40063  proththdlem  40068  stgoldbwt  40198  evengpop3  40214  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  pthdlem1  40972  lindslinindimp2lem3  42043  fllogbd  42152  nnolog2flm1  42182