Theorem syl5eqbrr 4473

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440

This theorem is referenced by:  enpr1g  7574  undom  7598  fidomdm  7794  prdom2  8375  infdif  8580  cfslb2n  8639  gchxpidm  9036  rankcf  9144  r1tskina  9149  tskuni  9150  ltsonq  9336  addgt0  10034  addgegt0  10035  addgtge0  10036  addge0  10037  expge1  12185  fsumrlim  13707  isumsup  13741  climcndslem1  13743  3dvds  14134  bitsinv1lem  14175  phicl2  14382  frgpnabllem1  17076  lt6abl  17096  pgpfaclem2  17328  unitmulcl  17508  gsumply1eq  18542  xrsdsreclblem  18659  znidomb  18773  lindfres  19025  2ndcdisj2  20124  hmphindis  20464  tsms0  20809  tgptsmscls  20818  metustexhalfOLD  21232  metustexhalf  21233  xrhmeo  21612  pcoass  21690  ovoliunlem1  22079  ismbl2  22104  voliunlem2  22127  ioombl1lem4  22137  itg2ge0  22308  itg2addlem  22331  itgge0  22383  dvfsumrlimge0  22597  abelthlem1  22992  abelthlem2  22993  pilem2  23013  rplogcl  23157  logge0  23158  argimgt0  23165  logdivlti  23173  logf1o2  23199  dvlog2lem  23201  ang180lem3  23342  atanlogaddlem  23441  atanlogsublem  23443  atantan  23451  atans2  23459  cxploglim2  23506  emcllem6  23528  emcllem7  23529  ftalem1  23544  ftalem2  23545  ppinncl  23646  chtrpcl  23647  vmalelog  23678  chtub  23685  logfacubnd  23694  logfacbnd3  23696  logfacrlim  23697  logexprlim  23698  mersenne  23700  perfectlem2  23703  bpos1lem  23755  bposlem1  23757  bposlem2  23758  bposlem3  23759  bposlem4  23760  bposlem5  23761  bposlem6  23762  lgseisen  23826  lgsquadlem1  23827  chebbnd1lem1  23852  chebbnd1lem3  23854  rpvmasumlem  23870  dchrvmasumlem2  23881  dchrvmasumlema  23883  dchrvmasumiflem1  23884  dchrisum0flblem2  23892  dchrisum0fno1  23894  dchrisum0re  23896  dirith2  23911  logdivsum  23916  mulog2sumlem1  23917  mulog2sumlem2  23918  log2sumbnd  23927  chpdifbndlem1  23936  chpdifbndlem2  23937  logdivbnd  23939  selberg3lem1  23940  pntpbnd1a  23968  pntpbnd2  23970  pntibndlem3  23975  pntlemn  23983  pntlemj  23986  pntlemk  23989  pnt  23997  tgldimor  24094  axlowdim  24466  minvecolem4  25994  dmct  27767  abrexct  27773  abrexctf  27775  nn0sqeq1  27793  nndiffz1  27830  xrge0addgt0  27915  esumcvg2  28316  inelcarsg  28519  carsgclctunlem2  28527  signsply0  28772  signsvtn  28805  lgamgulmlem2  28836  erdsze2lem2  28912  pellqrex  31054  reglogltb  31066  reglogleb  31067  rmspecsqrtnq  31081  rmspecnonsq  31082  rmspecpos  31091  areaquad  31425  hashnzfz2  31467  binomcxplemdvbinom  31499  binomcxplemnotnn0  31502  fmul01  31813  stoweidlem26  32047  stoweidlem44  32065  stoweidlem45  32066  wallispilem3  32088  wallispi  32091  stirlinglem11  32105  dirkertrigeqlem1  32119  dirkertrigeqlem3  32121  fourierdlem80  32208  fourierdlem102  32230  fourierdlem107  32235  fourierdlem114  32242  etransclem46  32302  nnolog2flm1  33465