Theorem syl5eqbrr 4471

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 4468	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1383   class class class wbr 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438

This theorem is referenced by:  enpr1g  7583  undom  7607  fidomdm  7804  prdom2  8387  infdif  8592  cfslb2n  8651  gchxpidm  9050  rankcf  9158  r1tskina  9163  tskuni  9164  ltsonq  9350  addgt0  10044  addgegt0  10045  addgtge0  10046  addge0  10047  expge1  12182  fsumrlim  13604  isumsup  13638  climcndslem1  13640  3dvds  13927  bitsinv1lem  13968  phicl2  14175  frgpnabllem1  16751  lt6abl  16771  pgpfaclem2  17007  unitmulcl  17187  gsumply1eq  18221  xrsdsreclblem  18338  znidomb  18473  lindfres  18731  2ndcdisj2  19831  hmphindis  20171  tsms0  20516  tgptsmscls  20525  metustexhalfOLD  20939  metustexhalf  20940  xrhmeo  21319  pcoass  21397  ovoliunlem1  21786  ismbl2  21811  voliunlem2  21834  ioombl1lem4  21844  itg2ge0  22015  itg2addlem  22038  itgge0  22090  dvfsumrlimge0  22304  abelthlem1  22698  abelthlem2  22699  pilem2  22719  rplogcl  22861  logge0  22862  argimgt0  22869  logdivlti  22877  logf1o2  22903  dvlog2lem  22905  ang180lem3  23015  atanlogaddlem  23116  atanlogsublem  23118  atantan  23126  atans2  23134  cxploglim2  23180  emcllem6  23202  emcllem7  23203  ftalem1  23218  ftalem2  23219  ppinncl  23320  chtrpcl  23321  vmalelog  23352  chtub  23359  logfacubnd  23368  logfacbnd3  23370  logfacrlim  23371  logexprlim  23372  mersenne  23374  perfectlem2  23377  bpos1lem  23429  bposlem1  23431  bposlem2  23432  bposlem3  23433  bposlem4  23434  bposlem5  23435  bposlem6  23436  lgseisen  23500  lgsquadlem1  23501  chebbnd1lem1  23526  chebbnd1lem3  23528  rpvmasumlem  23544  dchrvmasumlem2  23555  dchrvmasumlema  23557  dchrvmasumiflem1  23558  dchrisum0flblem2  23566  dchrisum0fno1  23568  dchrisum0re  23570  dirith2  23585  logdivsum  23590  mulog2sumlem1  23591  mulog2sumlem2  23592  log2sumbnd  23601  chpdifbndlem1  23610  chpdifbndlem2  23611  logdivbnd  23613  selberg3lem1  23614  pntpbnd1a  23642  pntpbnd2  23644  pntibndlem3  23649  pntlemn  23657  pntlemj  23660  pntlemk  23663  pnt  23671  tgldimor  23765  axlowdim  24136  minvecolem4  25668  dmct  27409  abrexct  27415  abrexctf  27417  nn0sqeq1  27434  nndiffz1  27468  xrge0addgt0  27554  esumcvg2  27966  signsply0  28381  signsvtn  28414  lgamgulmlem2  28445  erdsze2lem2  28521  pellqrex  30790  reglogltb  30802  reglogleb  30803  rmspecsqrtnq  30817  rmspecnonsq  30818  rmspecpos  30827  areaquad  31160  hashnzfz2  31202  fmul01  31502  stoweidlem26  31697  stoweidlem44  31715  stoweidlem45  31716  wallispilem3  31738  wallispi  31741  stirlinglem11  31755  dirkertrigeqlem1  31769  dirkertrigeqlem3  31771  fourierdlem80  31858  fourierdlem102  31880  fourierdlem107  31885  fourierdlem114  31892