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

Theorem syl5breqr 4059
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4058 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:  r1sdom  7446  alephordilem1  7700  mulge0  9291  xsubge0  10581  xmulgt0  10603  xmulge0  10604  xlemul1a  10608  sqlecan  11209  bernneq  11227  cnpart  11725  sqr0lem  11726  bitsfzo  12626  bitsmod  12627  bitsinv1lem  12632  pcge0  12914  prmreclem4  12966  prmreclem5  12967  isabvd  15585  abvtrivd  15605  nmolb2d  18227  nmoi  18237  nmoleub  18240  nmo0  18244  ovolge0  18840  itg1ge0a  19066  fta1g  19553  plyrem  19685  taylfval  19738  tayl0  19741  abelthlem2  19808  sinq12ge0  19876  relogrn  19919  logneg  19941  cxpge0  20030  amgmlem  20284  bposlem5  20527  lgsdir2lem2  20563  rpvmasumlem  20636  blocnilem  21382  pjssge0ii  22261  unierri  22684  esumcst  23436  eupath2lem3  23903  eupath2  23904  monotoddzzfi  27027  rmxypos  27034  rmygeid  27051  stoweidlem18  27767
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