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

Theorem syl6breq 4253
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 2438 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4245 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4214
This theorem is referenced by:  syl6breqr  4254  difsnen  7192  marypha1lem  7440  cda0en  8061  ackbij1lem5  8106  alephadd  8454  prlem934  8912  ltexprlem2  8916  recgt0ii  9918  discr  11518  faclbnd4lem1  11586  hashfun  11702  sqrlem7  12056  resqrex  12058  abs3lemi  12215  supcvg  12637  ege2le3  12694  cos01gt0  12794  sin02gt0  12795  bitsfzolem  12948  bitsmod  12950  prmreclem2  13287  efgi0  15354  efgi1  15355  dprdf1  15593  metustexhalfOLD  18595  metustexhalf  18596  nlmvscnlem2  18723  icccmplem2  18856  xrge0tsms  18867  iimulcl  18964  pcoass  19051  ipcnlem2  19200  ivthlem3  19352  vitalilem4  19505  vitali  19507  dvef  19866  ply1rem  20088  aaliou3lem2  20262  abelthlem8  20357  abelthlem9  20358  cosne0  20434  sinord  20438  tanregt0  20443  argimgt0  20509  logf1o2  20543  logtayllem  20552  cxpcn3lem  20633  ang180lem2  20654  ang180lem3  20655  atanlogsublem  20757  bndatandm  20771  leibpi  20784  emcllem6  20841  emcllem7  20842  ftalem5  20861  basellem7  20871  basellem9  20873  ppieq0  20961  ppiub  20990  chpeq0  20994  chpub  21006  logfacrlim  21010  logexprlim  21011  bposlem1  21070  bposlem2  21071  lgslem3  21084  lgsquadlem1  21140  lgsquadlem3  21142  chebbnd1lem3  21167  chtppilim  21171  chpchtlim  21175  dchrvmasumiflem1  21197  dchrisum0re  21209  mudivsum  21226  mulog2sumlem2  21231  pntibndlem2  21287  pntlemb  21293  pntlemh  21295  ostth3  21334  norm3lem  22653  nmopadjlem  23594  nmopcoadji  23606  hstle  23735  stadd3i  23753  strlem5  23760  xrge0iifcnv  24321  lgamgulmlem5  24819  lgamcvg2  24841  sinccvglem  25111  faclim2  25369  ismblfin  26249  irrapxlem2  26888  pellexlem2  26895  en2eleq  27360  en2other2  27361  f1otrspeq  27369  pmtrf  27376  pmtrmvd  27377  pmtrfinv  27381  fmul01  27688  clim1fr1  27705  stoweidlem14  27741  stoweidlem16  27743  stoweidlem26  27753  stoweidlem41  27768  stoweidlem42  27769  stoweidlem45  27772  wallispi  27797  stirlinglem1  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215
  Copyright terms: Public domain W3C validator