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

Theorem syl6breq 4476
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 2443 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4468 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  syl6breqr  4477  difsnen  7601  marypha1lem  7895  en2eleq  8389  en2other2  8390  cda0en  8562  ackbij1lem5  8607  alephadd  8955  prlem934  9414  ltexprlem2  9418  recgt0ii  10458  discr  12285  faclbnd4lem1  12353  hashfun  12477  sqrlem7  13064  resqrex  13066  abs3lemi  13224  supcvg  13649  ege2le3  13807  cos01gt0  13908  sin02gt0  13909  bitsfzolem  14066  bitsmod  14068  prmreclem2  14417  f1otrspeq  16451  pmtrf  16459  pmtrmvd  16460  pmtrfinv  16465  efgi0  16717  efgi1  16718  dprdf1  17059  metustexhalfOLD  21044  metustexhalf  21045  nlmvscnlem2  21172  icccmplem2  21306  xrge0tsms  21317  iimulcl  21415  pcoass  21502  ipcnlem2  21662  ivthlem3  21843  vitalilem4  21998  vitali  22000  dvef  22359  ply1rem  22542  aaliou3lem2  22717  abelthlem8  22812  abelthlem9  22813  cosne0  22895  sinord  22899  tanregt0  22904  argimgt0  22975  logf1o2  23009  logtayllem  23018  cxpcn3lem  23099  ang180lem2  23120  ang180lem3  23121  atanlogsublem  23224  bndatandm  23238  leibpi  23251  emcllem6  23308  emcllem7  23309  ftalem5  23328  basellem7  23338  basellem9  23340  ppieq0  23428  ppiub  23457  chpeq0  23461  chpub  23473  logfacrlim  23477  logexprlim  23478  bposlem1  23537  bposlem2  23538  lgslem3  23551  lgsquadlem1  23607  lgsquadlem3  23609  chebbnd1lem3  23634  chtppilim  23638  chpchtlim  23642  dchrvmasumiflem1  23664  dchrisum0re  23676  mudivsum  23693  mulog2sumlem2  23698  pntibndlem2  23754  pntlemb  23760  pntlemh  23762  ostth3  23801  norm3lem  26044  nmopadjlem  26986  nmopcoadji  26998  hstle  27127  stadd3i  27145  strlem5  27152  gsumle  27748  locfinreflem  27821  xrge0iifcnv  27893  signsply0  28486  signsvtp  28518  lgamgulmlem5  28553  lgamcvg2  28575  sinccvglem  29016  faclim2  29149  ismblfin  30031  irrapxlem2  30735  pellexlem2  30742  areaquad  31160  dvgrat  31169  fmul01  31528  clim1fr1  31561  sinaover2ne0  31622  stoweidlem14  31750  stoweidlem16  31752  stoweidlem26  31762  stoweidlem41  31777  stoweidlem42  31778  stoweidlem45  31781  wallispi  31806  stirlinglem1  31810  stirlinglem12  31821  fourierdlem24  31867  fourierdlem107  31950  fouriersw  31968  lincfsuppcl  32884  lincresunit3lem2  32951  lincresunit3  32952
  Copyright terms: Public domain W3C validator