Theorem syl5eqbrr 4689

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

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  enpr1g  8022  undom  8048  fidomdm  8243  prdom2  8829  infdif  9031  cfslb2n  9090  dmct  9346  gchxpidm  9491  rankcf  9599  r1tskina  9604  tskuni  9605  ltsonq  9791  addgt0  10514  addgegt0  10515  addgtge0  10516  addge0  10517  expge1  12897  fsumrlim  14543  isumsup  14579  climcndslem1  14581  3dvds  15052  3dvdsOLD  15053  bitsinv1lem  15163  phicl2  15473  frgpnabllem1  18276  lt6abl  18296  pgpfaclem2  18481  unitmulcl  18664  gsumply1eq  19675  xrsdsreclblem  19792  znidomb  19910  lindfres  20162  2ndcdisj2  21260  hmphindis  21600  tsms0  21945  tgptsmscls  21953  metustexhalf  22361  xrhmeo  22745  pcoass  22824  ovoliunlem1  23270  ismbl2  23295  voliunlem2  23319  ioombl1lem4  23329  itg2ge0  23502  itg2addlem  23525  itgge0  23577  dvfsumrlimge0  23793  abelthlem1  24185  abelthlem2  24186  pilem2  24206  rplogcl  24350  logge0  24351  argimgt0  24358  logdivlti  24366  logf1o2  24396  dvlog2lem  24398  ang180lem3  24541  atanlogaddlem  24640  atanlogsublem  24642  atantan  24650  atans2  24658  cxploglim2  24705  emcllem6  24727  emcllem7  24728  lgamgulmlem2  24756  ftalem1  24799  ftalem2  24800  ppinncl  24900  chtrpcl  24901  vmalelog  24930  chtub  24937  logfacubnd  24946  logfacbnd3  24948  logfacrlim  24949  logexprlim  24950  mersenne  24952  perfectlem2  24955  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  lgseisen  25104  lgsquadlem1  25105  chebbnd1lem1  25158  chebbnd1lem3  25160  rpvmasumlem  25176  dchrvmasumlem2  25187  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  dirith2  25217  logdivsum  25222  mulog2sumlem1  25223  mulog2sumlem2  25224  log2sumbnd  25233  chpdifbndlem1  25242  chpdifbndlem2  25243  logdivbnd  25245  selberg3lem1  25246  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem3  25281  pntlemn  25289  pntlemj  25292  pntlemk  25295  pnt  25303  tgldimor  25397  axlowdim  25841  minvecolem4  27736  abrexct  29494  abrexctf  29496  nn0sqeq1  29513  nndiffz1  29548  xrge0addgt0  29691  esumcvg2  30149  inelcarsg  30373  carsgclctunlem2  30381  signsply0  30628  signsvtn  30661  erdsze2lem2  31186  pellqrex  37443  reglogltb  37455  reglogleb  37456  rmspecsqrtnqOLD  37471  rmspecnonsq  37472  rmspecpos  37481  areaquad  37802  hashnzfz2  38520  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  fmul01  39812  climconstmpt  39890  stoweidlem26  40243  stoweidlem44  40261  stoweidlem45  40262  wallispilem3  40284  wallispi  40287  stirlinglem11  40301  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  fourierdlem80  40403  fourierdlem102  40425  fourierdlem107  40430  fourierdlem114  40437  etransclem46  40497  fmtnoge3  41442  fmtno4prmfac  41484  perfectALTVlem2  41631  gboge9  41652  mogoldbb  41673  tgoldbach  41705  tgoldbachOLD  41712  nnolog2flm1  42384