MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqbrr Structured version   Visualization version   GIF version

Theorem syl5eqbrr 4619
Description: A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
Hypotheses
Ref Expression
syl5eqbrr.1 𝐵 = 𝐴
syl5eqbrr.2 (𝜑𝐵𝑅𝐶)
Assertion
Ref Expression
syl5eqbrr (𝜑𝐴𝑅𝐶)

Proof of Theorem syl5eqbrr
StepHypRef Expression
1 syl5eqbrr.2 . 2 (𝜑𝐵𝑅𝐶)
2 syl5eqbrr.1 . 2 𝐵 = 𝐴
3 eqid 2610 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 4616 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  enpr1g  7908  undom  7933  fidomdm  8128  prdom2  8712  infdif  8914  cfslb2n  8973  gchxpidm  9370  rankcf  9478  r1tskina  9483  tskuni  9484  ltsonq  9670  addgt0  10393  addgegt0  10394  addgtge0  10395  addge0  10396  expge1  12759  fsumrlim  14384  isumsup  14418  climcndslem1  14420  3dvds  14890  3dvdsOLD  14891  bitsinv1lem  15001  phicl2  15311  frgpnabllem1  18099  lt6abl  18119  pgpfaclem2  18304  unitmulcl  18487  gsumply1eq  19496  xrsdsreclblem  19611  znidomb  19729  lindfres  19981  2ndcdisj2  21070  hmphindis  21410  tsms0  21755  tgptsmscls  21763  metustexhalf  22171  xrhmeo  22553  pcoass  22632  ovoliunlem1  23077  ismbl2  23102  voliunlem2  23126  ioombl1lem4  23136  itg2ge0  23308  itg2addlem  23331  itgge0  23383  dvfsumrlimge0  23597  abelthlem1  23989  abelthlem2  23990  pilem2  24010  rplogcl  24154  logge0  24155  argimgt0  24162  logdivlti  24170  logf1o2  24196  dvlog2lem  24198  ang180lem3  24341  atanlogaddlem  24440  atanlogsublem  24442  atantan  24450  atans2  24458  cxploglim2  24505  emcllem6  24527  emcllem7  24528  lgamgulmlem2  24556  ftalem1  24599  ftalem2  24600  ppinncl  24700  chtrpcl  24701  vmalelog  24730  chtub  24737  logfacubnd  24746  logfacbnd3  24748  logfacrlim  24749  logexprlim  24750  mersenne  24752  perfectlem2  24755  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  lgseisen  24904  lgsquadlem1  24905  chebbnd1lem1  24958  chebbnd1lem3  24960  rpvmasumlem  24976  dchrvmasumlem2  24987  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  dirith2  25017  logdivsum  25022  mulog2sumlem1  25023  mulog2sumlem2  25024  log2sumbnd  25033  chpdifbndlem1  25042  chpdifbndlem2  25043  logdivbnd  25045  selberg3lem1  25046  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem3  25081  pntlemn  25089  pntlemj  25092  pntlemk  25095  pnt  25103  tgldimor  25197  axlowdim  25641  minvecolem4  27120  dmct  28877  abrexct  28882  abrexctf  28884  nn0sqeq1  28901  nndiffz1  28936  xrge0addgt0  29022  esumcvg2  29476  inelcarsg  29700  carsgclctunlem2  29708  signsply0  29954  signsvtn  29987  erdsze2lem2  30440  pellqrex  36461  reglogltb  36473  reglogleb  36474  rmspecsqrtnqOLD  36489  rmspecnonsq  36490  rmspecpos  36499  areaquad  36821  hashnzfz2  37542  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  fmul01  38647  climconstmpt  38725  stoweidlem26  38919  stoweidlem44  38937  stoweidlem45  38938  wallispilem3  38960  wallispi  38963  stirlinglem11  38977  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  fourierdlem80  39079  fourierdlem102  39101  fourierdlem107  39106  fourierdlem114  39113  etransclem46  39173  fmtnoge3  39980  fmtno4prmfac  40022  perfectALTVlem2  40165  gboage9  40186  tgoldbach  40232  tgoldbachOLD  40239  nnolog2flm1  42182
  Copyright terms: Public domain W3C validator