Theorem syl5eqbrr 4323

Description: A 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 2441	. 2 |- C = C
4	1, 2, 3	3brtr3g 4320	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290

This theorem is referenced by:  enpr1g  7371  undom  7395  fidomdm  7589  prdom2  8169  infdif  8374  cfslb2n  8433  gchxpidm  8832  rankcf  8940  r1tskina  8945  tskuni  8946  ltsonq  9134  addgt0  9821  addgegt0  9822  addgtge0  9823  addge0  9824  expge1  11897  fsumrlim  13270  isumsup  13306  climcndslem1  13308  3dvds  13592  bitsinv1lem  13633  phicl2  13839  frgpnabllem1  16344  lt6abl  16364  pgpfaclem2  16573  unitmulcl  16746  xrsdsreclblem  17818  znidomb  17953  lindfres  18211  2ndcdisj2  19020  hmphindis  19329  tsms0  19674  tgptsmscls  19683  metustexhalfOLD  20097  metustexhalf  20098  xrhmeo  20477  pcoass  20555  ovoliunlem1  20944  ismbl2  20969  voliunlem2  20991  ioombl1lem4  21001  itg2ge0  21172  itg2addlem  21195  itgge0  21247  dvfsumrlimge0  21461  abelthlem1  21855  abelthlem2  21856  pilem2  21876  rplogcl  22012  logge0  22013  argimgt0  22020  logdivlti  22028  logf1o2  22054  dvlog2lem  22056  ang180lem3  22166  atanlogaddlem  22267  atanlogsublem  22269  atantan  22277  atans2  22285  cxploglim2  22331  emcllem6  22353  emcllem7  22354  ftalem1  22369  ftalem2  22370  ppinncl  22471  chtrpcl  22472  vmalelog  22503  chtub  22510  logfacubnd  22519  logfacbnd3  22521  logfacrlim  22522  logexprlim  22523  mersenne  22525  perfectlem2  22528  bpos1lem  22580  bposlem1  22582  bposlem2  22583  bposlem3  22584  bposlem4  22585  bposlem5  22586  bposlem6  22587  lgseisen  22651  lgsquadlem1  22652  chebbnd1lem1  22677  chebbnd1lem3  22679  rpvmasumlem  22695  dchrvmasumlem2  22706  dchrvmasumlema  22708  dchrvmasumiflem1  22709  dchrisum0flblem2  22717  dchrisum0fno1  22719  dchrisum0re  22721  dirith2  22736  logdivsum  22741  mulog2sumlem1  22742  mulog2sumlem2  22743  log2sumbnd  22752  chpdifbndlem1  22761  chpdifbndlem2  22762  logdivbnd  22764  selberg3lem1  22765  pntpbnd1a  22793  pntpbnd2  22795  pntibndlem3  22800  pntlemn  22808  pntlemj  22811  pntlemk  22814  pnt  22822  tgldimor  22914  axlowdim  23142  minvecolem4  24216  dmct  25949  abrexct  25955  abrexctf  25957  nndiffz1  26008  xrge0addgt0  26087  esumcvg2  26472  signsply0  26882  signsvtn  26915  lgamgulmlem2  26946  erdsze2lem2  27022  pellqrex  29145  reglogltb  29157  reglogleb  29158  rmspecsqrnq  29172  rmspecnonsq  29173  rmspecpos  29182  areaquad  29517  fmul01  29686  stoweidlem26  29746  stoweidlem44  29764  stoweidlem45  29765  wallispilem3  29787  wallispi  29790  stirlinglem11  29804