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

Theorem syl6breqr 4212
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 2408 . 2  |-  B  =  C
41, 3syl6breq 4211 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  pw2eng  7173  cda1en  8011  ackbij1lem9  8064  unsnen  8384  1nqenq  8795  gtndiv  10303  xov1plusxeqvd  10997  intfrac2  11194  serle  11333  discr1  11470  faclbnd4lem1  11539  sqrlem1  12003  sqrlem4  12006  sqrlem7  12009  supcvg  12590  ege2le3  12647  eirrlem  12758  ruclem12  12795  bitsfzo  12902  pcprendvds  13169  pcpremul  13172  pcfaclem  13222  infpnlem2  13234  yonedainv  14333  lmcn2  17634  hmph0  17780  icccmplem2  18807  reconnlem2  18811  xrge0tsms  18818  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  ivthlem2  19302  ivthlem3  19303  vitalilem2  19454  itg2seq  19587  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  c1liplem1  19833  lhop1lem  19850  dvcvx  19857  plyeq0lem  20082  radcnvcl  20286  radcnvle  20289  psercnlem1  20294  psercn  20295  pilem3  20322  tangtx  20366  cosne0  20385  recosf1o  20390  resinf1o  20391  efif1olem4  20400  logimul  20462  logcnlem3  20488  logf1o2  20494  ang180lem2  20605  acoscos  20686  emcllem7  20793  fsumharmonic  20803  ftalem2  20809  basellem1  20816  basellem2  20817  basellem3  20818  basellem5  20820  bposlem1  21021  bposlem2  21022  bposlem3  21023  lgsdirprm  21066  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  mulog2sumlem2  21182  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntlemc  21242  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemr  21249  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth3  21285  eupares  21650  eupap1  21651  siilem1  22305  minvecolem2  22330  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  nmopcoi  23551  staddi  23702  climlec3  25167  axsegconlem3  25762  cntotbnd  26395  jm2.27c  26968  fmul01  27577  stoweidlem36  27652  stoweidlem41  27657  wallispi2  27689  dalemply  30136  dalemsly  30137  dalem5  30149  dalem13  30158  dalem17  30162  dalem55  30209  dalem57  30211  lhpat3  30528  cdleme22aa  30821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator