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

Theorem syl6breq 4455
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 2461 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4447 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454   class class class wbr 4415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416
This theorem is referenced by:  syl6breqr  4456  difsnen  7679  marypha1lem  7972  en2eleq  8464  en2other2  8465  cda0en  8634  ackbij1lem5  8679  alephadd  9027  prlem934  9483  ltexprlem2  9487  recgt0ii  10539  discr  12440  faclbnd4lem1  12509  hashfun  12641  sqrlem7  13360  resqrex  13362  abs3lemi  13520  supcvg  13962  ege2le3  14192  cos01gt0  14293  sin02gt0  14294  bitsfzolem  14455  bitsfzolemOLD  14456  bitsmod  14458  prmreclem2  14909  f1otrspeq  17136  pmtrf  17144  pmtrmvd  17145  pmtrfinv  17150  efgi0  17418  efgi1  17419  dprdf1  17714  metustexhalf  21619  nlmvscnlem2  21736  icccmplem2  21889  xrge0tsms  21900  iimulcl  22013  pcoass  22103  ipcnlem2  22263  ivthlem3  22452  vitalilem4  22617  vitali  22619  dvef  22980  ply1rem  23162  aaliou3lem2  23347  abelthlem8  23442  abelthlem9  23443  cosne0  23527  sinord  23531  tanregt0  23536  argimgt0  23609  logf1o2  23643  logtayllem  23652  cxpcn3lem  23735  ang180lem2  23787  ang180lem3  23788  atanlogsublem  23889  bndatandm  23903  leibpi  23916  emcllem6  23974  emcllem7  23975  lgamgulmlem5  24006  lgamcvg2  24028  ftalem5  24049  ftalem5OLD  24051  basellem7  24061  basellem9  24063  ppieq0  24151  ppiub  24180  chpeq0  24184  chpub  24196  logfacrlim  24200  logexprlim  24201  bposlem1  24260  bposlem2  24261  lgslem3  24274  lgsquadlem1  24330  lgsquadlem3  24332  chebbnd1lem3  24357  chtppilim  24361  chpchtlim  24365  dchrvmasumiflem1  24387  dchrisum0re  24399  mudivsum  24416  mulog2sumlem2  24421  pntibndlem2  24477  pntlemb  24483  pntlemh  24485  ostth3  24524  norm3lem  26850  nmopadjlem  27790  nmopcoadji  27802  hstle  27931  stadd3i  27949  strlem5  27956  gsumle  28590  locfinreflem  28715  xrge0iifcnv  28787  carsggect  29198  omsmeas  29203  omsmeasOLD  29204  signsply0  29488  signsvtp  29520  sinccvglem  30364  faclim2  30432  poimirlem28  32012  ismblfin  32025  irrapxlem2  35711  pellexlem2  35718  areaquad  36145  dvgrat  36704  binomcxplemrat  36742  fmul01  37695  clim1fr1  37716  sinaover2ne0  37780  stoweidlem14  37911  stoweidlem16  37913  stoweidlem26  37923  stoweidlem41  37939  stoweidlem42  37940  stoweidlem45  37943  wallispi  37969  stirlinglem1  37973  stirlinglem12  37984  fourierdlem24  38030  fourierdlem107  38114  fouriersw  38132  lincfsuppcl  40478  lincresunit3lem2  40545  lincresunit3  40546
  Copyright terms: Public domain W3C validator