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

Theorem syl5eqbrr 4721
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 2651 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 4718 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  enpr1g  8063  undom  8089  fidomdm  8284  prdom2  8867  infdif  9069  cfslb2n  9128  dmct  9384  gchxpidm  9529  rankcf  9637  r1tskina  9642  tskuni  9643  ltsonq  9829  addgt0  10552  addgegt0  10553  addgtge0  10554  addge0  10555  expge1  12937  fsumrlim  14587  isumsup  14623  climcndslem1  14625  3dvds  15099  3dvdsOLD  15100  bitsinv1lem  15210  phicl2  15520  frgpnabllem1  18322  lt6abl  18342  pgpfaclem2  18527  unitmulcl  18710  gsumply1eq  19723  xrsdsreclblem  19840  znidomb  19958  lindfres  20210  2ndcdisj2  21308  hmphindis  21648  tsms0  21992  tgptsmscls  22000  metustexhalf  22408  xrhmeo  22792  pcoass  22870  ovoliunlem1  23316  ismbl2  23341  voliunlem2  23365  ioombl1lem4  23375  itg2ge0  23547  itg2addlem  23570  itgge0  23622  dvfsumrlimge0  23838  abelthlem1  24230  abelthlem2  24231  pilem2  24251  rplogcl  24395  logge0  24396  argimgt0  24403  logdivlti  24411  logf1o2  24441  dvlog2lem  24443  ang180lem3  24586  atanlogaddlem  24685  atanlogsublem  24687  atantan  24695  atans2  24703  cxploglim2  24750  emcllem6  24772  emcllem7  24773  lgamgulmlem2  24801  ftalem1  24844  ftalem2  24845  ppinncl  24945  chtrpcl  24946  vmalelog  24975  chtub  24982  logfacubnd  24991  logfacbnd3  24993  logfacrlim  24994  logexprlim  24995  mersenne  24997  perfectlem2  25000  bpos1lem  25052  bposlem1  25054  bposlem2  25055  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem6  25059  lgseisen  25149  lgsquadlem1  25150  chebbnd1lem1  25203  chebbnd1lem3  25205  rpvmasumlem  25221  dchrvmasumlem2  25232  dchrvmasumlema  25234  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  dirith2  25262  logdivsum  25267  mulog2sumlem1  25268  mulog2sumlem2  25269  log2sumbnd  25278  chpdifbndlem1  25287  chpdifbndlem2  25288  logdivbnd  25290  selberg3lem1  25291  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem3  25326  pntlemn  25334  pntlemj  25337  pntlemk  25340  pnt  25348  tgldimor  25442  axlowdim  25886  minvecolem4  27864  abrexct  29622  abrexctf  29624  nn0sqeq1  29641  nndiffz1  29676  xrge0addgt0  29819  esumcvg2  30277  inelcarsg  30501  carsgclctunlem2  30509  signsply0  30756  signsvtn  30789  erdsze2lem2  31312  pellqrex  37760  reglogltb  37772  reglogleb  37773  rmspecsqrtnqOLD  37788  rmspecnonsq  37789  rmspecpos  37798  areaquad  38119  hashnzfz2  38837  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  fmul01  40130  climconstmpt  40208  stoweidlem26  40561  stoweidlem44  40579  stoweidlem45  40580  wallispilem3  40602  wallispi  40605  stirlinglem11  40619  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  fourierdlem80  40721  fourierdlem102  40743  fourierdlem107  40748  fourierdlem114  40755  etransclem46  40815  fmtnoge3  41767  fmtno4prmfac  41809  perfectALTVlem2  41956  gboge9  41977  mogoldbb  41998  tgoldbach  42030  tgoldbachOLD  42037  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator