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

Theorem syl6breqr 4327
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 2442 . 2  |-  B  =  C
41, 3syl6breq 4326 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  pw2eng  7409  cda1en  8336  ackbij1lem9  8389  unsnen  8709  1nqenq  9123  gtndiv  10711  xov1plusxeqvd  11423  intfrac2  11689  serle  11853  discr1  11992  faclbnd4lem1  12061  sqrlem1  12724  sqrlem4  12727  sqrlem7  12730  supcvg  13310  ege2le3  13367  eirrlem  13478  ruclem12  13515  bitsfzo  13623  pcprendvds  13899  pcpremul  13902  pcfaclem  13952  infpnlem2  13964  yonedainv  15083  srgbinomlem4  16629  lmcn2  19197  hmph0  19343  icccmplem2  20375  reconnlem2  20379  xrge0tsms  20386  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  ivthlem2  20911  ivthlem3  20912  vitalilem2  21064  itg2seq  21195  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  dveflem  21426  dvferm1lem  21431  dvferm2lem  21433  c1liplem1  21443  lhop1lem  21460  dvcvx  21467  plyeq0lem  21653  radcnvcl  21857  radcnvle  21860  psercnlem1  21865  psercn  21866  pilem3  21893  tangtx  21942  cosne0  21961  recosf1o  21966  resinf1o  21967  efif1olem4  21976  logimul  22038  logcnlem3  22064  logf1o2  22070  ang180lem2  22181  heron  22208  acoscos  22263  emcllem7  22370  fsumharmonic  22380  ftalem2  22386  basellem1  22393  basellem2  22394  basellem3  22395  basellem5  22397  bposlem1  22598  bposlem2  22599  bposlem3  22600  lgsdirprm  22643  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  mulog2sumlem2  22759  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntlemc  22819  pntlemb  22821  pntlemg  22822  pntlemh  22823  pntlemr  22826  ostth2lem2  22858  ostth2lem3  22859  ostth2lem4  22860  ostth3  22862  axsegconlem3  23116  eupares  23547  eupap1  23548  siilem1  24202  minvecolem2  24227  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  nmopcoi  25450  staddi  25601  climlec3  27352  ftc1anclem8  28427  cntotbnd  28648  jm2.27c  29309  fmul01  29714  stoweidlem36  29784  stoweidlem41  29789  wallispi2  29821  clwlkisclwwlk2  30405  lincresunit3lem2  30903  lincresunit3  30904  dalemply  33138  dalemsly  33139  dalem5  33151  dalem13  33160  dalem17  33164  dalem55  33211  dalem57  33213  lhpat3  33530  cdleme22aa  33823
  Copyright terms: Public domain W3C validator