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

Theorem syl6breq 4319
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl6breq.1  |-  ( ph  ->  A R B )
syl6breq.2  |-  B  =  C
Assertion
Ref Expression
syl6breq  |-  ( ph  ->  A R C )

Proof of Theorem syl6breq
StepHypRef Expression
1 syl6breq.1 . 2  |-  ( ph  ->  A R B )
2 eqid 2433 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4311 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  syl6breqr  4320  difsnen  7381  marypha1lem  7671  en2eleq  8163  en2other2  8164  cda0en  8336  ackbij1lem5  8381  alephadd  8729  prlem934  9189  ltexprlem2  9193  recgt0ii  10225  discr  11984  faclbnd4lem1  12052  hashfun  12182  sqrlem7  12721  resqrex  12723  abs3lemi  12880  supcvg  13300  ege2le3  13357  cos01gt0  13457  sin02gt0  13458  bitsfzolem  13612  bitsmod  13614  prmreclem2  13960  f1otrspeq  15932  pmtrf  15940  pmtrmvd  15941  pmtrfinv  15946  efgi0  16196  efgi1  16197  dprdf1  16503  metustexhalfOLD  19979  metustexhalf  19980  nlmvscnlem2  20107  icccmplem2  20241  xrge0tsms  20252  iimulcl  20350  pcoass  20437  ipcnlem2  20597  ivthlem3  20778  vitalilem4  20932  vitali  20934  dvef  21293  ply1rem  21519  aaliou3lem2  21693  abelthlem8  21788  abelthlem9  21789  cosne0  21870  sinord  21874  tanregt0  21879  argimgt0  21945  logf1o2  21979  logtayllem  21988  cxpcn3lem  22069  ang180lem2  22090  ang180lem3  22091  atanlogsublem  22194  bndatandm  22208  leibpi  22221  emcllem6  22278  emcllem7  22279  ftalem5  22298  basellem7  22308  basellem9  22310  ppieq0  22398  ppiub  22427  chpeq0  22431  chpub  22443  logfacrlim  22447  logexprlim  22448  bposlem1  22507  bposlem2  22508  lgslem3  22521  lgsquadlem1  22577  lgsquadlem3  22579  chebbnd1lem3  22604  chtppilim  22608  chpchtlim  22612  dchrvmasumiflem1  22634  dchrisum0re  22646  mudivsum  22663  mulog2sumlem2  22668  pntibndlem2  22724  pntlemb  22730  pntlemh  22732  ostth3  22771  norm3lem  24373  nmopadjlem  25315  nmopcoadji  25327  hstle  25456  stadd3i  25474  strlem5  25481  xrge0iifcnv  26216  signsply0  26799  signsvtp  26831  lgamgulmlem5  26866  lgamcvg2  26888  sinccvglem  27163  faclim2  27400  ismblfin  28273  irrapxlem2  29006  pellexlem2  29013  areaquad  29434  fmul01  29603  clim1fr1  29617  stoweidlem14  29652  stoweidlem16  29654  stoweidlem26  29664  stoweidlem41  29679  stoweidlem42  29680  stoweidlem45  29683  wallispi  29708  stirlinglem1  29712  lincfsuppcl  30653  lincresunit3lem2  30720  lincresunit3  30721
  Copyright terms: Public domain W3C validator