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

Theorem breqtrrdi 5099
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 2828 . 2 𝐵 = 𝐶
41, 3breqtrdi 5098 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058
This theorem is referenced by:  enpr2d  8589  pw2eng  8615  undjudom  9585  dju1en  9589  djucomen  9595  djuassen  9596  xpdjuen  9597  infdjuabs  9620  ackbij1lem9  9642  unsnen  9967  1nqenq  10376  gtndiv  12051  xov1plusxeqvd  12876  intfrac2  13218  serle  13417  discr1  13592  faclbnd4lem1  13645  sqrlem1  14594  sqrlem4  14597  sqrlem7  14600  supcvg  15203  ege2le3  15435  eirrlem  15549  ruclem12  15586  bitsfzo  15776  pcprendvds  16169  pcpremul  16172  pcfaclem  16226  infpnlem2  16239  yonedainv  17523  srgbinomlem4  19285  lmcn2  22249  hmph0  22395  icccmplem2  23423  reconnlem2  23427  xrge0tsms  23434  minveclem2  24021  minveclem3b  24023  minveclem4  24027  minveclem6  24029  ivthlem2  24045  ivthlem3  24046  vitalilem2  24202  itg2seq  24335  itg2monolem1  24343  itg2monolem2  24344  itg2monolem3  24345  dveflem  24568  dvferm1lem  24573  dvferm2lem  24575  c1liplem1  24585  lhop1lem  24602  dvcvx  24609  plyeq0lem  24792  radcnvcl  24997  radcnvle  25000  psercnlem1  25005  psercn  25006  pilem3  25033  tangtx  25083  cos02pilt1  25103  cosne0  25106  recosf1o  25111  resinf1o  25112  efif1olem4  25121  logimul  25189  logcnlem3  25219  logf1o2  25225  ang180lem2  25380  heron  25408  acoscos  25463  emcllem7  25571  fsumharmonic  25581  ftalem2  25643  basellem1  25650  basellem2  25651  basellem3  25652  basellem5  25654  bposlem1  25852  bposlem2  25853  bposlem3  25854  lgsdirprm  25899  chebbnd1lem1  26037  chebbnd1lem2  26038  chebbnd1lem3  26039  mulog2sumlem2  26103  pntpbnd1a  26153  pntpbnd1  26154  pntpbnd2  26155  pntibndlem2  26159  pntlemc  26163  pntlemb  26165  pntlemg  26166  pntlemh  26167  pntlemr  26170  ostth2lem2  26202  ostth2lem3  26203  ostth2lem4  26204  ostth3  26206  axsegconlem3  26697  clwlkclwwlk2  27773  siilem1  28620  minvecolem2  28644  minvecolem4  28649  minvecolem5  28650  minvecolem6  28651  nmopcoi  29864  staddi  30015  cycpmco2lem4  30764  cycpmco2lem5  30765  hgt750lemd  31912  climlec3  32958  logi  32959  poimirlem26  34910  ftc1anclem8  34966  cntotbnd  35066  dalemply  36782  dalemsly  36783  dalem5  36795  dalem13  36804  dalem17  36808  dalem55  36855  dalem57  36857  lhpat3  37174  cdleme22aa  37467  jm2.27c  39595  hashnzfz2  40644  supxrubd  41371  suprnmpt  41420  fzisoeu  41557  upbdrech  41562  recnnltrp  41635  uzublem  41694  fmul01  41851  limsupubuzlem  41983  limsupequzmptlem  41999  ioodvbdlimc1lem2  42207  ioodvbdlimc2lem  42209  stoweidlem36  42312  stoweidlem41  42317  wallispi2  42349  dirkercncflem1  42379  fourierdlem6  42389  fourierdlem7  42390  fourierdlem19  42402  fourierdlem20  42403  fourierdlem24  42407  fourierdlem25  42408  fourierdlem26  42409  fourierdlem30  42413  fourierdlem31  42414  fourierdlem42  42425  fourierdlem47  42429  fourierdlem48  42430  fourierdlem63  42445  fourierdlem64  42446  fourierdlem65  42447  fourierdlem71  42453  fourierdlem79  42461  fourierdlem89  42471  fourierdlem90  42472  fourierdlem91  42473  fouriersw  42507  etransclem28  42538  etransclem48  42558  hoidmv1lelem1  42864  hoidmv1lelem3  42866  hoidmvlelem1  42868  hoidmvlelem4  42871  bgoldbtbndlem2  43962  lincresunit3lem2  44526  lincresunit3  44527  resum2sqgt0  44685  amgmwlem  44894
  Copyright terms: Public domain W3C validator