Theorem syl5eqbrr 4451

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

Syntax hints:   -> wi 4   = wceq 1455   class class class wbr 4416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417

This theorem is referenced by:  enpr1g  7661  undom  7686  fidomdm  7879  prdom2  8463  infdif  8665  cfslb2n  8724  gchxpidm  9120  rankcf  9228  r1tskina  9233  tskuni  9234  ltsonq  9420  addgt0  10128  addgegt0  10129  addgtge0  10130  addge0  10131  expge1  12341  fsumrlim  13920  isumsup  13954  climcndslem1  13956  3dvds  14418  bitsinv1lem  14464  phicl2  14765  frgpnabllem1  17558  lt6abl  17578  pgpfaclem2  17764  unitmulcl  17941  gsumply1eq  18948  xrsdsreclblem  19063  znidomb  19181  lindfres  19430  2ndcdisj2  20521  hmphindis  20861  tsms0  21205  tgptsmscls  21213  metustexhalf  21620  xrhmeo  22023  pcoass  22104  ovoliunlem1  22504  ismbl2  22530  voliunlem2  22553  ioombl1lem4  22563  itg2ge0  22742  itg2addlem  22765  itgge0  22817  dvfsumrlimge0  23031  abelthlem1  23435  abelthlem2  23436  pilem2  23456  pilem2OLD  23457  rplogcl  23602  logge0  23603  argimgt0  23610  logdivlti  23618  logf1o2  23644  dvlog2lem  23646  ang180lem3  23789  atanlogaddlem  23888  atanlogsublem  23890  atantan  23898  atans2  23906  cxploglim2  23953  emcllem6  23975  emcllem7  23976  lgamgulmlem2  24004  ftalem1  24046  ftalem2  24047  ppinncl  24150  chtrpcl  24151  vmalelog  24182  chtub  24189  logfacubnd  24198  logfacbnd3  24200  logfacrlim  24201  logexprlim  24202  mersenne  24204  perfectlem2  24207  bpos1lem  24259  bposlem1  24261  bposlem2  24262  bposlem3  24263  bposlem4  24264  bposlem5  24265  bposlem6  24266  lgseisen  24330  lgsquadlem1  24331  chebbnd1lem1  24356  chebbnd1lem3  24358  rpvmasumlem  24374  dchrvmasumlem2  24385  dchrvmasumlema  24387  dchrvmasumiflem1  24388  dchrisum0flblem2  24396  dchrisum0fno1  24398  dchrisum0re  24400  dirith2  24415  logdivsum  24420  mulog2sumlem1  24421  mulog2sumlem2  24422  log2sumbnd  24431  chpdifbndlem1  24440  chpdifbndlem2  24441  logdivbnd  24443  selberg3lem1  24444  pntpbnd1a  24472  pntpbnd2  24474  pntibndlem3  24479  pntlemn  24487  pntlemj  24490  pntlemk  24493  pnt  24501  tgldimor  24595  axlowdim  25040  minvecolem4  26571  minvecolem4OLD  26581  dmct  28347  abrexct  28353  abrexctf  28355  nn0sqeq1  28373  nndiffz1  28415  xrge0addgt0  28503  esumcvg2  28957  inelcarsg  29192  carsgclctunlem2  29200  signsply0  29489  signsvtn  29522  erdsze2lem2  29976  pellqrex  35771  reglogltb  35784  reglogleb  35785  rmspecsqrtnq  35799  rmspecnonsq  35800  rmspecpos  35809  areaquad  36146  hashnzfz2  36714  binomcxplemdvbinom  36746  binomcxplemnotnn0  36749  fmul01  37696  stoweidlem26  37924  stoweidlem44  37943  stoweidlem45  37944  wallispilem3  37967  wallispi  37970  stirlinglem11  37984  dirkertrigeqlem1  37998  dirkertrigeqlem3  38000  fourierdlem80  38088  fourierdlem102  38110  fourierdlem107  38115  fourierdlem114  38122  etransclem46  38183  perfectALTVlem2  38882  gboage9  38903  tgoldbach  38949  nnolog2flm1  40674