Theorem syl5eqbrr 4206

Description: B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)

Hypotheses

Ref	Expression
syl5eqbrr.1	|- B = A
syl5eqbrr.2	|- ( ph -> B R C )

Assertion

Ref	Expression
syl5eqbrr	|- ( ph -> A R C )

Proof of Theorem syl5eqbrr

Step	Hyp	Ref	Expression
1		syl5eqbrr.2	. 2 |- ( ph -> B R C )
2		syl5eqbrr.1	. 2 |- B = A
3		eqid 2404	. 2 |- C = C
4	1, 2, 3	3brtr3g 4203	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1649   class class class wbr 4172

This theorem is referenced by:  enpr1g  7132  undom  7155  fidomdm  7347  prdom2  7846  infdif  8045  cfslb2n  8104  gchxpidm  8500  rankcf  8608  r1tskina  8613  tskuni  8614  ltsonq  8802  addgt0  9470  addgegt0  9471  addgtge0  9472  addge0  9473  expge1  11372  fsumrlim  12545  isumsup  12582  climcndslem1  12584  3dvds  12867  bitsinv1lem  12908  phicl2  13112  frgpnabllem1  15439  lt6abl  15459  pgpfaclem2  15595  unitmulcl  15724  xrsdsreclblem  16699  znidomb  16797  2ndcdisj2  17473  hmphindis  17782  metustexhalfOLD  18546  metustexhalf  18547  xrhmeo  18924  pcoass  19002  ovoliunlem1  19351  ismbl2  19376  voliunlem2  19398  ioombl1lem4  19408  itg2ge0  19580  itg2addlem  19603  itgge0  19655  dvfsumrlimge0  19867  abelthlem1  20300  abelthlem2  20301  pilem2  20321  rplogcl  20452  logge0  20453  argimgt0  20460  logdivlti  20468  logf1o2  20494  dvlog2lem  20496  ang180lem3  20606  atanlogaddlem  20706  atanlogsublem  20708  atantan  20716  atans2  20724  cxploglim2  20770  emcllem6  20792  emcllem7  20793  ftalem1  20808  ftalem2  20809  ppinncl  20910  chtrpcl  20911  vmalelog  20942  chtub  20949  logfacubnd  20958  logfacbnd3  20960  logfacrlim  20961  logexprlim  20962  mersenne  20964  perfectlem2  20967  bpos1lem  21019  bposlem1  21021  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  lgseisen  21090  lgsquadlem1  21091  chebbnd1lem1  21116  chebbnd1lem3  21118  rpvmasumlem  21134  dchrvmasumlem2  21145  dchrvmasumlema  21147  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0re  21160  dirith2  21175  logdivsum  21180  mulog2sumlem1  21181  mulog2sumlem2  21182  log2sumbnd  21191  chpdifbndlem1  21200  chpdifbndlem2  21201  logdivbnd  21203  selberg3lem1  21204  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem3  21239  pntlemn  21247  pntlemj  21250  pntlemk  21253  pnt  21261  minvecolem4  22335  dmct  24059  abrexct  24064  abrexctf  24066  xrge0addgt0  24167  esumcvg2  24430  lgamgulmlem2  24767  erdsze2lem2  24843  axlowdim  25804  pellqrex  26832  reglogltb  26844  reglogleb  26845  rmspecsqrnq  26859  rmspecnonsq  26860  rmspecpos  26869  lindfres  27161  fmul01  27577  stoweidlem26  27642  stoweidlem44  27660  stoweidlem45  27661  wallispilem3  27683  wallispi  27686  stirlinglem11  27700

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173