Theorem syl5eqbrr 4331

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 2443	. 2 |- C = C
4	1, 2, 3	3brtr3g 4328	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1369   class class class wbr 4297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298

This theorem is referenced by:  enpr1g  7380  undom  7404  fidomdm  7598  prdom2  8178  infdif  8383  cfslb2n  8442  gchxpidm  8841  rankcf  8949  r1tskina  8954  tskuni  8955  ltsonq  9143  addgt0  9830  addgegt0  9831  addgtge0  9832  addge0  9833  expge1  11906  fsumrlim  13279  isumsup  13315  climcndslem1  13317  3dvds  13601  bitsinv1lem  13642  phicl2  13848  frgpnabllem1  16356  lt6abl  16376  pgpfaclem2  16588  unitmulcl  16761  xrsdsreclblem  17864  znidomb  17999  lindfres  18257  2ndcdisj2  19066  hmphindis  19375  tsms0  19720  tgptsmscls  19729  metustexhalfOLD  20143  metustexhalf  20144  xrhmeo  20523  pcoass  20601  ovoliunlem1  20990  ismbl2  21015  voliunlem2  21037  ioombl1lem4  21047  itg2ge0  21218  itg2addlem  21241  itgge0  21293  dvfsumrlimge0  21507  abelthlem1  21901  abelthlem2  21902  pilem2  21922  rplogcl  22058  logge0  22059  argimgt0  22066  logdivlti  22074  logf1o2  22100  dvlog2lem  22102  ang180lem3  22212  atanlogaddlem  22313  atanlogsublem  22315  atantan  22323  atans2  22331  cxploglim2  22377  emcllem6  22399  emcllem7  22400  ftalem1  22415  ftalem2  22416  ppinncl  22517  chtrpcl  22518  vmalelog  22549  chtub  22556  logfacubnd  22565  logfacbnd3  22567  logfacrlim  22568  logexprlim  22569  mersenne  22571  perfectlem2  22574  bpos1lem  22626  bposlem1  22628  bposlem2  22629  bposlem3  22630  bposlem4  22631  bposlem5  22632  bposlem6  22633  lgseisen  22697  lgsquadlem1  22698  chebbnd1lem1  22723  chebbnd1lem3  22725  rpvmasumlem  22741  dchrvmasumlem2  22752  dchrvmasumlema  22754  dchrvmasumiflem1  22755  dchrisum0flblem2  22763  dchrisum0fno1  22765  dchrisum0re  22767  dirith2  22782  logdivsum  22787  mulog2sumlem1  22788  mulog2sumlem2  22789  log2sumbnd  22798  chpdifbndlem1  22807  chpdifbndlem2  22808  logdivbnd  22810  selberg3lem1  22811  pntpbnd1a  22839  pntpbnd2  22841  pntibndlem3  22846  pntlemn  22854  pntlemj  22857  pntlemk  22860  pnt  22868  tgldimor  22960  axlowdim  23212  minvecolem4  24286  dmct  26019  abrexct  26025  abrexctf  26027  nndiffz1  26080  xrge0addgt0  26159  esumcvg2  26541  signsply0  26957  signsvtn  26990  lgamgulmlem2  27021  erdsze2lem2  27097  pellqrex  29225  reglogltb  29237  reglogleb  29238  rmspecsqrnq  29252  rmspecnonsq  29253  rmspecpos  29262  areaquad  29597  fmul01  29766  stoweidlem26  29826  stoweidlem44  29844  stoweidlem45  29845  wallispilem3  29867  wallispi  29870  stirlinglem11  29884