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

Theorem syl6breqr 4727
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 2660 . 2 𝐵 = 𝐶
41, 3syl6breq 4726 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686
This theorem is referenced by:  pw2eng  8107  cda1en  9035  ackbij1lem9  9088  unsnen  9413  1nqenq  9822  gtndiv  11492  xov1plusxeqvd  12356  intfrac2  12697  serle  12896  discr1  13040  faclbnd4lem1  13120  sqrlem1  14027  sqrlem4  14030  sqrlem7  14033  supcvg  14632  ege2le3  14864  eirrlem  14976  ruclem12  15014  bitsfzo  15204  pcprendvds  15592  pcpremul  15595  pcfaclem  15649  infpnlem2  15662  yonedainv  16968  srgbinomlem4  18589  lmcn2  21500  hmph0  21646  icccmplem2  22673  reconnlem2  22677  xrge0tsms  22684  minveclem2  23243  minveclem3b  23245  minveclem4  23249  minveclem6  23251  ivthlem2  23267  ivthlem3  23268  vitalilem2  23423  itg2seq  23554  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  dveflem  23787  dvferm1lem  23792  dvferm2lem  23794  c1liplem1  23804  lhop1lem  23821  dvcvx  23828  plyeq0lem  24011  radcnvcl  24216  radcnvle  24219  psercnlem1  24224  psercn  24225  pilem3  24252  tangtx  24302  cosne0  24321  recosf1o  24326  resinf1o  24327  efif1olem4  24336  logimul  24405  logcnlem3  24435  logf1o2  24441  ang180lem2  24585  heron  24610  acoscos  24665  emcllem7  24773  fsumharmonic  24783  ftalem2  24845  basellem1  24852  basellem2  24853  basellem3  24854  basellem5  24856  bposlem1  25054  bposlem2  25055  bposlem3  25056  lgsdirprm  25101  chebbnd1lem1  25203  chebbnd1lem2  25204  chebbnd1lem3  25205  mulog2sumlem2  25269  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntlemc  25329  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemr  25336  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth3  25372  axsegconlem3  25844  clwlkclwwlk2  26969  siilem1  27834  minvecolem2  27859  minvecolem4  27864  minvecolem5  27865  minvecolem6  27866  nmopcoi  29082  staddi  29233  hgt750lemd  30854  climlec3  31745  logi  31746  poimirlem26  33565  ftc1anclem8  33622  cntotbnd  33725  dalemply  35258  dalemsly  35259  dalem5  35271  dalem13  35280  dalem17  35284  dalem55  35331  dalem57  35333  lhpat3  35650  cdleme22aa  35944  jm2.27c  37891  hashnzfz2  38837  supxrubd  39611  suprnmpt  39669  fzisoeu  39828  upbdrech  39833  recnnltrp  39906  uzublem  39970  fmul01  40130  limsupubuzlem  40262  limsupequzmptlem  40278  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem36  40571  stoweidlem41  40576  wallispi2  40608  dirkercncflem1  40638  fourierdlem6  40648  fourierdlem7  40649  fourierdlem19  40661  fourierdlem20  40662  fourierdlem24  40666  fourierdlem25  40667  fourierdlem26  40668  fourierdlem30  40672  fourierdlem31  40673  fourierdlem42  40684  fourierdlem47  40688  fourierdlem48  40689  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem71  40712  fourierdlem79  40720  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fouriersw  40766  etransclem28  40797  etransclem48  40817  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidmvlelem4  41133  bgoldbtbndlem2  42019  lincresunit3lem2  42594  lincresunit3  42595  amgmwlem  42876
  Copyright terms: Public domain W3C validator