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

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

Proof of Theorem eqbrtrrid
StepHypRef Expression
1 eqbrtrrid.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrrid.1 . 2 𝐵 = 𝐴
3 eqid 2733 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 5142 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110
This theorem is referenced by:  enpr1g  8970  undom  9009  undomOLD  9010  fidomdm  9279  prdom2  9950  infdju1  10133  infdif  10153  cfslb2n  10212  fin56  10337  dmct  10468  gchxpidm  10613  rankcf  10721  r1tskina  10726  tskuni  10727  ltsonq  10913  addgt0  11649  addgegt0  11650  addgtge0  11651  addge0  11652  expge1  14014  fsumrlim  15704  isumsup  15740  climcndslem1  15742  fprodge1  15886  3dvds  16221  bitsinv1lem  16329  phicl2  16648  frgpnabllem1  19659  lt6abl  19680  pgpfaclem2  19869  unitmulcl  20101  xrsdsreclblem  20866  znidomb  20991  lindfres  21252  gsumply1eq  21699  2ndcdisj2  22831  hmphindis  23171  tsms0  23516  tgptsmscls  23524  metustexhalf  23935  xrhmeo  24332  pcoass  24410  ovoliunlem1  24889  ismbl2  24914  voliunlem2  24938  ioombl1lem4  24948  itg2ge0  25123  itg2addlem  25146  itgge0  25198  dvfsumrlimge0  25417  abelthlem1  25813  abelthlem2  25814  pilem2  25834  cos0pilt1  25911  rplogcl  25982  logge0  25983  argimgt0  25990  logdivlti  25998  logf1o2  26028  dvlog2lem  26030  ang180lem3  26184  atanlogaddlem  26286  atanlogsublem  26288  atantan  26296  atans2  26304  cxploglim2  26351  emcllem6  26373  emcllem7  26374  lgamgulmlem2  26402  ftalem1  26445  ftalem2  26446  ppinncl  26546  chtrpcl  26547  vmalelog  26576  chtub  26583  logfacubnd  26592  logfacbnd3  26594  logfacrlim  26595  logexprlim  26596  mersenne  26598  perfectlem2  26601  bpos1lem  26653  bposlem1  26655  bposlem2  26656  bposlem3  26657  bposlem4  26658  bposlem5  26659  bposlem6  26660  lgseisen  26750  lgsquadlem1  26751  chebbnd1lem1  26840  chebbnd1lem3  26842  rpvmasumlem  26858  dchrvmasumlem2  26869  dchrvmasumlema  26871  dchrvmasumiflem1  26872  dchrisum0flblem2  26880  dchrisum0fno1  26882  dchrisum0re  26884  dirith2  26899  logdivsum  26904  mulog2sumlem1  26905  mulog2sumlem2  26906  log2sumbnd  26915  chpdifbndlem1  26924  chpdifbndlem2  26925  logdivbnd  26927  selberg3lem1  26928  pntpbnd1a  26956  pntpbnd2  26958  pntibndlem3  26963  pntlemn  26971  pntlemj  26974  pntlemk  26977  pnt  26985  tgldimor  27493  axlowdim  27959  minvecolem4  29871  abrexct  31687  abrexctf  31689  nndiffz1  31743  wrdt2ind  31863  xrge0addgt0  31938  drngdimgt0  32377  esumcvg2  32750  inelcarsg  32975  carsgclctunlem2  32983  signsply0  33227  signsvtn  33260  erdsze2lem2  33862  lcmineqlem23  40558  lcmineqlem  40559  aks4d1p1p6  40580  aks4d1p1  40583  metakunt2  40628  metakunt29  40655  2xp3dxp2ge1d  40664  flt4lem7  41044  pellqrex  41249  reglogltb  41261  reglogleb  41262  rmspecnonsq  41277  rmspecpos  41287  areaquad  41597  hashnzfz2  42693  binomcxplemdvbinom  42725  binomcxplemnotnn0  42728  fmul01  43911  climconstmpt  43989  stoweidlem26  44357  stoweidlem44  44375  stoweidlem45  44376  wallispilem3  44398  wallispi  44401  stirlinglem11  44415  dirkertrigeqlem1  44429  dirkertrigeqlem3  44431  fourierdlem80  44517  fourierdlem102  44539  fourierdlem107  44544  fourierdlem114  44551  etransclem46  44611  fmtnoge3  45812  fmtno4prmfac  45854  perfectALTVlem2  46004  gboge9  46046  mogoldbb  46067  tgoldbach  46099  nnolog2flm1  46766
  Copyright terms: Public domain W3C validator