Theorem syl5eqbrr 4481

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

Syntax hints:   -> wi 4   = wceq 1379   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448

This theorem is referenced by:  enpr1g  7578  undom  7602  fidomdm  7798  prdom2  8380  infdif  8585  cfslb2n  8644  gchxpidm  9043  rankcf  9151  r1tskina  9156  tskuni  9157  ltsonq  9343  addgt0  10034  addgegt0  10035  addgtge0  10036  addge0  10037  expge1  12167  fsumrlim  13584  isumsup  13618  climcndslem1  13620  3dvds  13905  bitsinv1lem  13946  phicl2  14153  frgpnabllem1  16668  lt6abl  16688  pgpfaclem2  16923  unitmulcl  17097  gsumply1eq  18118  xrsdsreclblem  18232  znidomb  18367  lindfres  18625  2ndcdisj2  19724  hmphindis  20033  tsms0  20378  tgptsmscls  20387  metustexhalfOLD  20801  metustexhalf  20802  xrhmeo  21181  pcoass  21259  ovoliunlem1  21648  ismbl2  21673  voliunlem2  21696  ioombl1lem4  21706  itg2ge0  21877  itg2addlem  21900  itgge0  21952  dvfsumrlimge0  22166  abelthlem1  22560  abelthlem2  22561  pilem2  22581  rplogcl  22717  logge0  22718  argimgt0  22725  logdivlti  22733  logf1o2  22759  dvlog2lem  22761  ang180lem3  22871  atanlogaddlem  22972  atanlogsublem  22974  atantan  22982  atans2  22990  cxploglim2  23036  emcllem6  23058  emcllem7  23059  ftalem1  23074  ftalem2  23075  ppinncl  23176  chtrpcl  23177  vmalelog  23208  chtub  23215  logfacubnd  23224  logfacbnd3  23226  logfacrlim  23227  logexprlim  23228  mersenne  23230  perfectlem2  23233  bpos1lem  23285  bposlem1  23287  bposlem2  23288  bposlem3  23289  bposlem4  23290  bposlem5  23291  bposlem6  23292  lgseisen  23356  lgsquadlem1  23357  chebbnd1lem1  23382  chebbnd1lem3  23384  rpvmasumlem  23400  dchrvmasumlem2  23411  dchrvmasumlema  23413  dchrvmasumiflem1  23414  dchrisum0flblem2  23422  dchrisum0fno1  23424  dchrisum0re  23426  dirith2  23441  logdivsum  23446  mulog2sumlem1  23447  mulog2sumlem2  23448  log2sumbnd  23457  chpdifbndlem1  23466  chpdifbndlem2  23467  logdivbnd  23469  selberg3lem1  23470  pntpbnd1a  23498  pntpbnd2  23500  pntibndlem3  23505  pntlemn  23513  pntlemj  23516  pntlemk  23519  pnt  23527  tgldimor  23621  axlowdim  23940  minvecolem4  25472  dmct  27209  abrexct  27215  abrexctf  27217  nndiffz1  27264  xrge0addgt0  27343  esumcvg2  27733  signsply0  28148  signsvtn  28181  lgamgulmlem2  28212  erdsze2lem2  28288  pellqrex  30419  reglogltb  30431  reglogleb  30432  rmspecsqrtnq  30446  rmspecnonsq  30447  rmspecpos  30456  areaquad  30789  hashnzfz2  30826  fmul01  31130  stoweidlem26  31326  stoweidlem44  31344  stoweidlem45  31345  wallispilem3  31367  wallispi  31370  stirlinglem11  31384  fourierdlem107  31514