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

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

Proof of Theorem syl6breqr
StepHypRef Expression
1 syl6breqr.1 . 2 (𝜑𝐴𝑅𝐵)
2 syl6breqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2615 . 2 𝐵 = 𝐶
41, 3syl6breq 4615 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575
This theorem is referenced by:  pw2eng  7925  cda1en  8854  ackbij1lem9  8907  unsnen  9228  1nqenq  9637  gtndiv  11283  xov1plusxeqvd  12142  intfrac2  12471  serle  12670  discr1  12814  faclbnd4lem1  12894  sqrlem1  13774  sqrlem4  13777  sqrlem7  13780  supcvg  14370  ege2le3  14602  eirrlem  14714  ruclem12  14752  bitsfzo  14938  pcprendvds  15326  pcpremul  15329  pcfaclem  15383  infpnlem2  15396  yonedainv  16687  srgbinomlem4  18309  lmcn2  21201  hmph0  21347  icccmplem2  22363  reconnlem2  22367  xrge0tsms  22374  minveclem2  22919  minveclem3b  22921  minveclem4  22925  minveclem6  22927  ivthlem2  22942  ivthlem3  22943  vitalilem2  23098  itg2seq  23229  itg2monolem1  23237  itg2monolem2  23238  itg2monolem3  23239  dveflem  23460  dvferm1lem  23465  dvferm2lem  23467  c1liplem1  23477  lhop1lem  23494  dvcvx  23501  plyeq0lem  23684  radcnvcl  23889  radcnvle  23892  psercnlem1  23897  psercn  23898  pilem3  23925  tangtx  23975  cosne0  23994  recosf1o  23999  resinf1o  24000  efif1olem4  24009  logimul  24078  logcnlem3  24104  logf1o2  24110  ang180lem2  24254  heron  24279  acoscos  24334  emcllem7  24442  fsumharmonic  24452  ftalem2  24514  basellem1  24521  basellem2  24522  basellem3  24523  basellem5  24525  bposlem1  24723  bposlem2  24724  bposlem3  24725  lgsdirprm  24770  chebbnd1lem1  24872  chebbnd1lem2  24873  chebbnd1lem3  24874  mulog2sumlem2  24938  pntpbnd1a  24988  pntpbnd1  24989  pntpbnd2  24990  pntibndlem2  24994  pntlemc  24998  pntlemb  25000  pntlemg  25001  pntlemh  25002  pntlemr  25005  ostth2lem2  25037  ostth2lem3  25038  ostth2lem4  25039  ostth3  25041  axsegconlem3  25514  clwlkisclwwlk2  26081  eupares  26265  eupap1  26266  siilem1  26893  minvecolem2  26918  minvecolem4  26923  minvecolem5  26924  minvecolem6  26925  nmopcoi  28141  staddi  28292  climlec3  30675  logi  30676  poimirlem26  32405  ftc1anclem8  32462  cntotbnd  32565  dalemply  33758  dalemsly  33759  dalem5  33771  dalem13  33780  dalem17  33784  dalem55  33831  dalem57  33833  lhpat3  34150  cdleme22aa  34445  jm2.27c  36392  hashnzfz2  37342  supxrubd  38128  suprnmpt  38150  fzisoeu  38255  upbdrech  38260  recnnltrp  38335  fmul01  38448  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  stoweidlem36  38730  stoweidlem41  38735  wallispi2  38767  dirkercncflem1  38797  fourierdlem6  38807  fourierdlem7  38808  fourierdlem19  38820  fourierdlem20  38821  fourierdlem24  38825  fourierdlem25  38826  fourierdlem26  38827  fourierdlem30  38831  fourierdlem31  38832  fourierdlem42  38843  fourierdlem47  38847  fourierdlem48  38848  fourierdlem63  38863  fourierdlem64  38864  fourierdlem65  38865  fourierdlem71  38871  fourierdlem79  38879  fourierdlem89  38889  fourierdlem90  38890  fourierdlem91  38891  fouriersw  38925  etransclem28  38956  etransclem48  38976  hoidmv1lelem1  39282  hoidmv1lelem3  39284  hoidmvlelem1  39286  hoidmvlelem4  39289  bgoldbtbndlem2  40024  clwlkclwwlk2  41211  lincresunit3lem2  42062  lincresunit3  42063  amgmwlem  42317
  Copyright terms: Public domain W3C validator