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

Theorem syl6breq 4062
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 2283 . 2  |-  A  =  A
3 syl6breq.2 . 2  |-  B  =  C
41, 2, 33brtr3g 4054 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  syl6breqr  4063  difsnen  6944  marypha1lem  7186  cda0en  7805  ackbij1lem5  7850  alephadd  8199  prlem934  8657  ltexprlem2  8661  recgt0ii  9662  discr  11238  faclbnd4lem1  11306  hashfun  11389  sqrlem7  11734  resqrex  11736  abs3lemi  11893  supcvg  12314  ege2le3  12371  cos01gt0  12471  sin02gt0  12472  bitsfzolem  12625  bitsmod  12627  prmreclem2  12964  efgi0  15029  efgi1  15030  dprdf1  15268  nlmvscnlem2  18196  icccmplem2  18328  xrge0tsms  18339  iimulcl  18435  pcoass  18522  ipcnlem2  18671  ivthlem3  18813  vitalilem4  18966  vitali  18968  dvef  19327  ply1rem  19549  aaliou3lem2  19723  abelthlem8  19815  abelthlem9  19816  cosne0  19892  sinord  19896  tanregt0  19901  argimgt0  19966  logf1o2  19997  logtayllem  20006  cxpcn3lem  20087  ang180lem2  20108  ang180lem3  20109  atanlogsublem  20211  bndatandm  20225  leibpi  20238  emcllem6  20294  emcllem7  20295  ftalem5  20314  basellem7  20324  basellem9  20326  ppieq0  20414  ppiub  20443  chpeq0  20447  chpub  20459  logfacrlim  20463  logexprlim  20464  bposlem1  20523  bposlem2  20524  lgslem3  20537  lgsquadlem1  20593  lgsquadlem3  20595  chebbnd1lem3  20620  chtppilim  20624  chpchtlim  20628  dchrvmasumiflem1  20650  dchrisum0re  20662  mudivsum  20679  mulog2sumlem2  20684  pntibndlem2  20740  pntlemb  20746  pntlemh  20748  ostth3  20787  norm3lem  21728  nmopadjlem  22669  nmopcoadji  22681  hstle  22810  stadd3i  22828  strlem5  22835  xrge0iifcnv  23315  sinccvglem  24005  cntrset  25602  irrapxlem2  26908  pellexlem2  26915  en2eleq  27381  en2other2  27382  f1otrspeq  27390  pmtrf  27397  pmtrmvd  27398  pmtrfinv  27402  fmul01  27710  clim1fr1  27727  stoweidlem14  27763  stoweidlem16  27765  stoweidlem26  27775  stoweidlem41  27790  stoweidlem45  27794  stoweidlem51  27800
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator