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

Theorem syl6breq 4078
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 2296 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4070 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  syl6breqr  4079  difsnen  6960  marypha1lem  7202  cda0en  7821  ackbij1lem5  7866  alephadd  8215  prlem934  8673  ltexprlem2  8677  recgt0ii  9678  discr  11254  faclbnd4lem1  11322  hashfun  11405  sqrlem7  11750  resqrex  11752  abs3lemi  11909  supcvg  12330  ege2le3  12387  cos01gt0  12487  sin02gt0  12488  bitsfzolem  12641  bitsmod  12643  prmreclem2  12980  efgi0  15045  efgi1  15046  dprdf1  15284  nlmvscnlem2  18212  icccmplem2  18344  xrge0tsms  18355  iimulcl  18451  pcoass  18538  ipcnlem2  18687  ivthlem3  18829  vitalilem4  18982  vitali  18984  dvef  19343  ply1rem  19565  aaliou3lem2  19739  abelthlem8  19831  abelthlem9  19832  cosne0  19908  sinord  19912  tanregt0  19917  argimgt0  19982  logf1o2  20013  logtayllem  20022  cxpcn3lem  20103  ang180lem2  20124  ang180lem3  20125  atanlogsublem  20227  bndatandm  20241  leibpi  20254  emcllem6  20310  emcllem7  20311  ftalem5  20330  basellem7  20340  basellem9  20342  ppieq0  20430  ppiub  20459  chpeq0  20463  chpub  20475  logfacrlim  20479  logexprlim  20480  bposlem1  20539  bposlem2  20540  lgslem3  20553  lgsquadlem1  20609  lgsquadlem3  20611  chebbnd1lem3  20636  chtppilim  20640  chpchtlim  20644  dchrvmasumiflem1  20666  dchrisum0re  20678  mudivsum  20695  mulog2sumlem2  20700  pntibndlem2  20756  pntlemb  20762  pntlemh  20764  ostth3  20803  norm3lem  21744  nmopadjlem  22685  nmopcoadji  22697  hstle  22826  stadd3i  22844  strlem5  22851  xrge0iifcnv  23330  sinccvglem  24020  cntrset  25705  irrapxlem2  27011  pellexlem2  27018  en2eleq  27484  en2other2  27485  f1otrspeq  27493  pmtrf  27500  pmtrmvd  27501  pmtrfinv  27505  fmul01  27813  clim1fr1  27830  stoweidlem14  27866  stoweidlem16  27868  stoweidlem26  27878  stoweidlem41  27893  stoweidlem45  27897  stoweidlem51  27903
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator