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

Theorem breqtrrdi 5152
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
breqtrrdi.1 (𝜑𝐴𝑅𝐵)
breqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
breqtrrdi (𝜑𝐴𝑅𝐶)

Proof of Theorem breqtrrdi
StepHypRef Expression
1 breqtrrdi.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2746 . 2 𝐵 = 𝐶
41, 3breqtrdi 5151 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5110
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111
This theorem is referenced by:  enpr2d  9000  enpr2dOLD  9001  pw2eng  9029  undjudom  10110  dju1en  10114  djucomen  10120  djuassen  10121  xpdjuen  10122  infdjuabs  10149  ackbij1lem9  10171  unsnen  10496  1nqenq  10905  gtndiv  12587  xov1plusxeqvd  13422  intfrac2  13770  serle  13970  discr1  14149  faclbnd4lem1  14200  01sqrexlem1  15134  01sqrexlem4  15137  01sqrexlem7  15140  supcvg  15748  ege2le3  15979  eirrlem  16093  ruclem12  16130  bitsfzo  16322  pcprendvds  16719  pcpremul  16722  pcfaclem  16777  infpnlem2  16790  yonedainv  18177  srgbinomlem4  19967  lmcn2  23016  hmph0  23162  icccmplem2  24202  reconnlem2  24206  xrge0tsms  24213  minveclem2  24806  minveclem3b  24808  minveclem4  24812  minveclem6  24814  ivthlem2  24832  ivthlem3  24833  vitalilem2  24989  itg2seq  25123  itg2monolem1  25131  itg2monolem2  25132  itg2monolem3  25133  dveflem  25359  dvferm1lem  25364  dvferm2lem  25366  c1liplem1  25376  lhop1lem  25393  dvcvx  25400  plyeq0lem  25587  radcnvcl  25792  radcnvle  25795  psercnlem1  25800  psercn  25801  pilem3  25828  tangtx  25878  cos02pilt1  25898  cosne0  25901  recosf1o  25907  resinf1o  25908  efif1olem4  25917  logimul  25985  logcnlem3  26015  logf1o2  26021  ang180lem2  26176  heron  26204  acoscos  26259  emcllem7  26367  fsumharmonic  26377  ftalem2  26439  basellem1  26446  basellem2  26447  basellem3  26448  basellem5  26450  bposlem1  26648  bposlem2  26649  bposlem3  26650  lgsdirprm  26695  chebbnd1lem1  26833  chebbnd1lem2  26834  chebbnd1lem3  26835  mulog2sumlem2  26899  pntpbnd1a  26949  pntpbnd1  26950  pntpbnd2  26951  pntibndlem2  26955  pntlemc  26959  pntlemb  26961  pntlemg  26962  pntlemh  26963  pntlemr  26966  ostth2lem2  26998  ostth2lem3  26999  ostth2lem4  27000  ostth3  27002  axsegconlem3  27910  clwlkclwwlk2  28989  siilem1  29835  minvecolem2  29859  minvecolem4  29864  minvecolem5  29865  minvecolem6  29866  nmopcoi  31079  staddi  31230  cycpmco2lem4  32020  cycpmco2lem5  32021  hgt750lemd  33301  climlec3  34345  logi  34346  poimirlem26  36133  ftc1anclem8  36187  cntotbnd  36284  dalemply  38146  dalemsly  38147  dalem5  38159  dalem13  38168  dalem17  38172  dalem55  38219  dalem57  38221  lhpat3  38538  cdleme22aa  38831  aks4d1p1p7  40560  jm2.27c  41360  hashnzfz2  42675  supxrubd  43397  suprnmpt  43465  fzisoeu  43608  upbdrech  43613  recnnltrp  43685  uzublem  43739  fmul01  43895  limsupubuzlem  44027  limsupequzmptlem  44043  ioodvbdlimc1lem2  44247  ioodvbdlimc2lem  44249  stoweidlem36  44351  stoweidlem41  44356  wallispi2  44388  dirkercncflem1  44418  fourierdlem6  44428  fourierdlem7  44429  fourierdlem19  44441  fourierdlem20  44442  fourierdlem24  44446  fourierdlem25  44447  fourierdlem26  44448  fourierdlem30  44452  fourierdlem31  44453  fourierdlem42  44464  fourierdlem47  44468  fourierdlem48  44469  fourierdlem63  44484  fourierdlem64  44485  fourierdlem65  44486  fourierdlem71  44492  fourierdlem79  44500  fourierdlem89  44510  fourierdlem90  44511  fourierdlem91  44512  fouriersw  44546  etransclem28  44577  etransclem48  44597  hoidmv1lelem1  44906  hoidmv1lelem3  44908  hoidmvlelem1  44910  hoidmvlelem4  44913  bgoldbtbndlem2  46072  lincresunit3lem2  46635  lincresunit3  46636  resum2sqgt0  46867  amgmwlem  47323
  Copyright terms: Public domain W3C validator