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

Theorem syl5breqr 4208
Description: B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl5breqr.1  |-  A R B
syl5breqr.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
syl5breqr  |-  ( ph  ->  A R C )

Proof of Theorem syl5breqr
StepHypRef Expression
1 syl5breqr.1 . 2  |-  A R B
2 syl5breqr.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2409 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4207 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  r1sdom  7656  alephordilem1  7910  mulge0  9501  xsubge0  10796  xmulgt0  10818  xmulge0  10819  xlemul1a  10823  sqlecan  11442  bernneq  11460  hashge1  11618  cnpart  12000  sqr0lem  12001  bitsfzo  12902  bitsmod  12903  bitsinv1lem  12908  pcge0  13190  prmreclem4  13242  prmreclem5  13243  isabvd  15863  abvtrivd  15883  nmolb2d  18705  nmoi  18715  nmoleub  18718  nmo0  18722  ovolge0  19330  itg1ge0a  19556  fta1g  20043  plyrem  20175  taylfval  20228  abelthlem2  20301  sinq12ge0  20369  relogrn  20412  logneg  20435  cxpge0  20527  amgmlem  20781  bposlem5  21025  lgsdir2lem2  21061  rpvmasumlem  21134  eupath2lem3  21654  eupath2  21655  blocnilem  22258  pjssge0ii  23137  unierri  23560  esumcst  24408  ballotlem5  24710  itgaddnclem2  26163  monotoddzzfi  26895  rmxypos  26902  rmygeid  26919  stoweidlem18  27634  stoweidlem55  27671  wallispi2lem1  27687  frgrawopreglem2  28148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator