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

Theorem syl5eqbrr 4613
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 2609 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 4610 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  enpr1g  7885  undom  7910  fidomdm  8105  prdom2  8689  infdif  8891  cfslb2n  8950  gchxpidm  9347  rankcf  9455  r1tskina  9460  tskuni  9461  ltsonq  9647  addgt0  10363  addgegt0  10364  addgtge0  10365  addge0  10366  expge1  12714  fsumrlim  14330  isumsup  14364  climcndslem1  14366  3dvds  14836  3dvdsOLD  14837  bitsinv1lem  14947  phicl2  15257  frgpnabllem1  18045  lt6abl  18065  pgpfaclem2  18250  unitmulcl  18433  gsumply1eq  19442  xrsdsreclblem  19557  znidomb  19674  lindfres  19923  2ndcdisj2  21012  hmphindis  21352  tsms0  21697  tgptsmscls  21705  metustexhalf  22112  xrhmeo  22484  pcoass  22563  ovoliunlem1  22994  ismbl2  23019  voliunlem2  23043  ioombl1lem4  23053  itg2ge0  23225  itg2addlem  23248  itgge0  23300  dvfsumrlimge0  23514  abelthlem1  23906  abelthlem2  23907  pilem2  23927  rplogcl  24071  logge0  24072  argimgt0  24079  logdivlti  24087  logf1o2  24113  dvlog2lem  24115  ang180lem3  24258  atanlogaddlem  24357  atanlogsublem  24359  atantan  24367  atans2  24375  cxploglim2  24422  emcllem6  24444  emcllem7  24445  lgamgulmlem2  24473  ftalem1  24516  ftalem2  24517  ppinncl  24617  chtrpcl  24618  vmalelog  24647  chtub  24654  logfacubnd  24663  logfacbnd3  24665  logfacrlim  24666  logexprlim  24667  mersenne  24669  perfectlem2  24672  bpos1lem  24724  bposlem1  24726  bposlem2  24727  bposlem3  24728  bposlem4  24729  bposlem5  24730  bposlem6  24731  lgseisen  24821  lgsquadlem1  24822  chebbnd1lem1  24875  chebbnd1lem3  24877  rpvmasumlem  24893  dchrvmasumlem2  24904  dchrvmasumlema  24906  dchrvmasumiflem1  24907  dchrisum0flblem2  24915  dchrisum0fno1  24917  dchrisum0re  24919  dirith2  24934  logdivsum  24939  mulog2sumlem1  24940  mulog2sumlem2  24941  log2sumbnd  24950  chpdifbndlem1  24959  chpdifbndlem2  24960  logdivbnd  24962  selberg3lem1  24963  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem3  24998  pntlemn  25006  pntlemj  25009  pntlemk  25012  pnt  25020  tgldimor  25114  axlowdim  25559  minvecolem4  26926  dmct  28683  abrexct  28688  abrexctf  28690  nn0sqeq1  28707  nndiffz1  28742  xrge0addgt0  28828  esumcvg2  29282  inelcarsg  29506  carsgclctunlem2  29514  signsply0  29760  signsvtn  29793  erdsze2lem2  30246  pellqrex  36257  reglogltb  36269  reglogleb  36270  rmspecsqrtnqOLD  36285  rmspecnonsq  36286  rmspecpos  36295  areaquad  36617  hashnzfz2  37338  binomcxplemdvbinom  37370  binomcxplemnotnn0  37373  fmul01  38444  climconstmpt  38522  stoweidlem26  38716  stoweidlem44  38734  stoweidlem45  38735  wallispilem3  38757  wallispi  38760  stirlinglem11  38774  dirkertrigeqlem1  38788  dirkertrigeqlem3  38790  fourierdlem80  38876  fourierdlem102  38898  fourierdlem107  38903  fourierdlem114  38910  etransclem46  38970  fmtnoge3  39778  fmtno4prmfac  39820  perfectALTVlem2  39963  gboage9  39984  tgoldbach  40030  tgoldbachOLD  40037  nnolog2flm1  42177
  Copyright terms: Public domain W3C validator