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

Theorem breqtrdi 5072
 Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
breqtrdi.1 (𝜑𝐴𝑅𝐵)
breqtrdi.2 𝐵 = 𝐶
Assertion
Ref Expression
breqtrdi (𝜑𝐴𝑅𝐶)

Proof of Theorem breqtrdi
StepHypRef Expression
1 breqtrdi.1 . 2 (𝜑𝐴𝑅𝐵)
2 eqid 2798 . 2 𝐴 = 𝐴
3 breqtrdi.2 . 2 𝐵 = 𝐶
41, 2, 33brtr3g 5064 1 (𝜑𝐴𝑅𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032 This theorem is referenced by:  breqtrrdi  5073  difsnen  8585  marypha1lem  8884  en2eleq  9422  en2other2  9423  dju0en  9589  pwdju1  9604  pwdjudom  9630  ackbij1lem5  9638  alephadd  9991  prlem934  10447  ltexprlem2  10451  recgt0ii  11538  discr  13600  faclbnd4lem1  13652  hashfun  13797  sqrlem7  14603  resqrex  14605  abs3lemi  14765  supcvg  15206  ege2le3  15438  cos01gt0  15539  sin02gt0  15540  bitsfzolem  15776  bitsmod  15778  prmreclem2  16246  f1otrspeq  18571  pmtrf  18579  pmtrmvd  18580  pmtrfinv  18585  efgi0  18842  efgi1  18843  dprdf1  19152  metustexhalf  23173  nlmvscnlem2  23301  icccmplem2  23438  xrge0tsms  23449  iimulcl  23552  pcoass  23639  ipcnlem2  23858  ivthlem3  24067  vitalilem4  24225  vitali  24227  dvef  24593  ply1rem  24774  aaliou3lem2  24949  abelthlem8  25044  abelthlem9  25045  cosne0  25131  sinord  25136  tanregt0  25141  argimgt0  25213  logf1o2  25251  logtayllem  25260  cxpcn3lem  25346  ang180lem2  25406  ang180lem3  25407  atanlogsublem  25511  bndatandm  25525  leibpi  25538  emcllem6  25596  emcllem7  25597  lgamgulmlem5  25628  lgamcvg2  25650  ftalem5  25672  basellem7  25682  basellem9  25684  ppieq0  25771  ppiub  25798  chpeq0  25802  chpub  25814  logfacrlim  25818  logexprlim  25819  bposlem1  25878  bposlem2  25879  lgslem3  25893  lgsquadlem1  25974  lgsquadlem3  25976  chebbnd1lem3  26065  chtppilim  26069  chpchtlim  26073  dchrvmasumiflem1  26095  dchrisum0re  26107  mudivsum  26124  mulog2sumlem2  26129  pntibndlem2  26185  pntlemb  26191  pntlemh  26193  ostth3  26232  crctcshwlkn0  27617  norm3lem  28942  nmopadjlem  29882  nmopcoadji  29894  hstle  30023  stadd3i  30041  strlem5  30048  pfxlsw2ccat  30662  gsumle  30785  locfinreflem  31208  xrge0iifcnv  31301  carsggect  31701  omsmeas  31706  signsply0  31946  signsvtp  31978  tgoldbachgtd  32058  sinccvglem  33043  faclim2  33108  poimirlem28  35104  ismblfin  35117  sn-0lt1  39630  sn-inelr  39633  dffltz  39658  irrapxlem2  39807  pellexlem2  39814  areaquad  40209  dvgrat  41059  binomcxplemrat  41097  fmul01  42265  clim1fr1  42286  sinaover2ne0  42553  stoweidlem14  42699  stoweidlem16  42701  stoweidlem26  42711  stoweidlem41  42726  stoweidlem42  42727  stoweidlem45  42730  wallispi  42755  stirlinglem1  42759  stirlinglem12  42770  fourierdlem24  42816  fourierdlem107  42898  fouriersw  42916  meaiunincf  43165  meaiuninc3  43167  lincfsuppcl  44863  lincresunit3lem2  44930  lincresunit3  44931
 Copyright terms: Public domain W3C validator