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

Theorem syl6breqr 4063
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 2287 . 2  |-  B  =  C
41, 3syl6breq 4062 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  pw2eng  6968  cda1en  7801  ackbij1lem9  7854  unsnen  8175  1nqenq  8586  gtndiv  10089  xov1plusxeqvd  10780  intfrac2  10962  serle  11101  discr1  11237  faclbnd4lem1  11306  sqrlem1  11728  sqrlem4  11731  sqrlem7  11734  supcvg  12314  ege2le3  12371  eirrlem  12482  ruclem12  12519  bitsfzo  12626  pcprendvds  12893  pcpremul  12896  pcfaclem  12946  infpnlem2  12958  yonedainv  14055  lmcn2  17343  hmph0  17486  icccmplem2  18328  reconnlem2  18332  xrge0tsms  18339  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  ivthlem2  18812  ivthlem3  18813  vitalilem2  18964  itg2seq  19097  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  c1liplem1  19343  lhop1lem  19360  dvcvx  19367  plyeq0lem  19592  radcnvcl  19793  radcnvle  19796  psercnlem1  19801  psercn  19802  pilem3  19829  tangtx  19873  cosne0  19892  recosf1o  19897  resinf1o  19898  efif1olem4  19907  logimul  19968  logcnlem3  19991  logf1o2  19997  ang180lem2  20108  acoscos  20189  emcllem7  20295  fsumharmonic  20305  ftalem2  20311  basellem1  20318  basellem2  20319  basellem3  20320  basellem5  20322  bposlem1  20523  bposlem2  20524  bposlem3  20525  lgsdirprm  20568  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  mulog2sumlem2  20684  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntlemc  20744  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemr  20751  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth3  20787  siilem1  21429  minvecolem2  21454  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  nmopcoi  22675  staddi  22826  eupares  23899  eupap1  23900  axsegconlem3  24547  cntotbnd  26520  jm2.27c  27100  fmul01  27710  stoweidlem36  27785  stoweidlem41  27790  dalemply  29843  dalemsly  29844  dalem5  29856  dalem13  29865  dalem17  29869  dalem55  29916  dalem57  29918  lhpat3  30235  cdleme22aa  30528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator