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

Theorem syl6breqr 4487
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6breqr.1  |-  ( ph  ->  A R B )
syl6breqr.2  |-  C  =  B
Assertion
Ref Expression
syl6breqr  |-  ( ph  ->  A R C )

Proof of Theorem syl6breqr
StepHypRef Expression
1 syl6breqr.1 . 2  |-  ( ph  ->  A R B )
2 syl6breqr.2 . . 3  |-  C  =  B
32eqcomi 2480 . 2  |-  B  =  C
41, 3syl6breq 4486 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  pw2eng  7623  cda1en  8555  ackbij1lem9  8608  unsnen  8928  1nqenq  9340  gtndiv  10938  xov1plusxeqvd  11666  intfrac2  11953  serle  12130  discr1  12270  faclbnd4lem1  12339  sqrlem1  13039  sqrlem4  13042  sqrlem7  13045  supcvg  13630  ege2le3  13687  eirrlem  13798  ruclem12  13835  bitsfzo  13944  pcprendvds  14223  pcpremul  14226  pcfaclem  14276  infpnlem2  14288  yonedainv  15408  srgbinomlem4  16996  lmcn2  19913  hmph0  20059  icccmplem2  21091  reconnlem2  21095  xrge0tsms  21102  minveclem2  21604  minveclem3b  21606  minveclem4  21610  minveclem6  21612  ivthlem2  21627  ivthlem3  21628  vitalilem2  21781  itg2seq  21912  itg2monolem1  21920  itg2monolem2  21921  itg2monolem3  21922  dveflem  22143  dvferm1lem  22148  dvferm2lem  22150  c1liplem1  22160  lhop1lem  22177  dvcvx  22184  plyeq0lem  22370  radcnvcl  22574  radcnvle  22577  psercnlem1  22582  psercn  22583  pilem3  22610  tangtx  22659  cosne0  22678  recosf1o  22683  resinf1o  22684  efif1olem4  22693  logimul  22755  logcnlem3  22781  logf1o2  22787  ang180lem2  22898  heron  22925  acoscos  22980  emcllem7  23087  fsumharmonic  23097  ftalem2  23103  basellem1  23110  basellem2  23111  basellem3  23112  basellem5  23114  bposlem1  23315  bposlem2  23316  bposlem3  23317  lgsdirprm  23360  chebbnd1lem1  23410  chebbnd1lem2  23411  chebbnd1lem3  23412  mulog2sumlem2  23476  pntpbnd1a  23526  pntpbnd1  23527  pntpbnd2  23528  pntibndlem2  23532  pntlemc  23536  pntlemb  23538  pntlemg  23539  pntlemh  23540  pntlemr  23543  ostth2lem2  23575  ostth2lem3  23576  ostth2lem4  23577  ostth3  23579  axsegconlem3  23926  clwlkisclwwlk2  24494  eupares  24679  eupap1  24680  siilem1  25470  minvecolem2  25495  minvecolem4  25500  minvecolem5  25501  minvecolem6  25502  nmopcoi  26718  staddi  26869  climlec3  28625  ftc1anclem8  29702  cntotbnd  29923  jm2.27c  30581  hashnzfz2  30854  fmul01  31158  stoweidlem36  31364  stoweidlem41  31369  wallispi2  31401  fourierdlem30  31465  usgedgleordALT  31915  lincresunit3lem2  32180  lincresunit3  32181  dalemply  34468  dalemsly  34469  dalem5  34481  dalem13  34490  dalem17  34494  dalem55  34541  dalem57  34543  lhpat3  34860  cdleme22aa  35153
  Copyright terms: Public domain W3C validator