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

Theorem eqbrtrrid 5098
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 2825 . 2 𝐶 = 𝐶
41, 2, 33brtr3g 5095 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063
This theorem is referenced by:  enpr1g  8567  undom  8597  fidomdm  8793  prdom2  9424  infdju1  9607  infdif  9623  cfslb2n  9682  fin56  9807  dmct  9938  gchxpidm  10083  rankcf  10191  r1tskina  10196  tskuni  10197  ltsonq  10383  addgt0  11118  addgegt0  11119  addgtge0  11120  addge0  11121  expge1  13459  fsumrlim  15158  isumsup  15194  climcndslem1  15196  fprodge1  15341  3dvds  15672  bitsinv1lem  15782  phicl2  16097  frgpnabllem1  18915  lt6abl  18937  pgpfaclem2  19126  unitmulcl  19336  gsumply1eq  20390  xrsdsreclblem  20507  znidomb  20624  lindfres  20883  2ndcdisj2  21981  hmphindis  22321  tsms0  22665  tgptsmscls  22673  metustexhalf  23081  xrhmeo  23465  pcoass  23543  ovoliunlem1  24018  ismbl2  24043  voliunlem2  24067  ioombl1lem4  24077  itg2ge0  24251  itg2addlem  24274  itgge0  24326  dvfsumrlimge0  24542  abelthlem1  24934  abelthlem2  24935  pilem2  24955  rplogcl  25100  logge0  25101  argimgt0  25108  logdivlti  25116  logf1o2  25146  dvlog2lem  25148  ang180lem3  25302  atanlogaddlem  25404  atanlogsublem  25406  atantan  25414  atans2  25422  cxploglim2  25470  emcllem6  25492  emcllem7  25493  lgamgulmlem2  25521  ftalem1  25564  ftalem2  25565  ppinncl  25665  chtrpcl  25666  vmalelog  25695  chtub  25702  logfacubnd  25711  logfacbnd3  25713  logfacrlim  25714  logexprlim  25715  mersenne  25717  perfectlem2  25720  bpos1lem  25772  bposlem1  25774  bposlem2  25775  bposlem3  25776  bposlem4  25777  bposlem5  25778  bposlem6  25779  lgseisen  25869  lgsquadlem1  25870  chebbnd1lem1  25959  chebbnd1lem3  25961  rpvmasumlem  25977  dchrvmasumlem2  25988  dchrvmasumlema  25990  dchrvmasumiflem1  25991  dchrisum0flblem2  25999  dchrisum0fno1  26001  dchrisum0re  26003  dirith2  26018  logdivsum  26023  mulog2sumlem1  26024  mulog2sumlem2  26025  log2sumbnd  26034  chpdifbndlem1  26043  chpdifbndlem2  26044  logdivbnd  26046  selberg3lem1  26047  pntpbnd1a  26075  pntpbnd2  26077  pntibndlem3  26082  pntlemn  26090  pntlemj  26093  pntlemk  26096  pnt  26104  tgldimor  26202  axlowdim  26661  minvecolem4  28571  abrexct  30365  abrexctf  30367  nndiffz1  30422  wrdt2ind  30541  xrge0addgt0  30592  drngdimgt0  30902  esumcvg2  31232  inelcarsg  31455  carsgclctunlem2  31463  signsply0  31707  signsvtn  31740  erdsze2lem2  32335  pellqrex  39337  reglogltb  39349  reglogleb  39350  rmspecnonsq  39365  rmspecpos  39374  areaquad  39684  hashnzfz2  40514  binomcxplemdvbinom  40546  binomcxplemnotnn0  40549  fmul01  41722  climconstmpt  41800  stoweidlem26  42173  stoweidlem44  42191  stoweidlem45  42192  wallispilem3  42214  wallispi  42217  stirlinglem11  42231  dirkertrigeqlem1  42245  dirkertrigeqlem3  42247  fourierdlem80  42333  fourierdlem102  42355  fourierdlem107  42360  fourierdlem114  42367  etransclem46  42427  fmtnoge3  43520  fmtno4prmfac  43562  perfectALTVlem2  43715  gboge9  43757  mogoldbb  43778  tgoldbach  43810  nnolog2flm1  44478
  Copyright terms: Public domain W3C validator