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

Theorem syl5breqr 4403
Description: A 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 2390 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4402 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   class class class wbr 4367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368
This theorem is referenced by:  r1sdom  8105  alephordilem1  8367  mulge0  9988  xsubge0  11374  xmulgt0  11396  xmulge0  11397  xlemul1a  11401  sqlecan  12177  bernneq  12194  hashge1  12360  hashge2el2dif  12425  cnpart  13075  sqr0lem  13076  bitsfzo  14087  bitsmod  14088  bitsinv1lem  14093  pcge0  14387  prmreclem4  14439  prmreclem5  14440  isabvd  17582  abvtrivd  17602  isnzr2hash  18025  nmolb2d  21310  nmoi  21320  nmoleub  21323  nmo0  21327  ovolge0  21977  itg1ge0a  22203  fta1g  22653  plyrem  22786  taylfval  22839  abelthlem2  22912  sinq12ge0  22986  relogrn  23034  logneg  23060  cxpge0  23151  amgmlem  23436  bposlem5  23680  lgsdir2lem2  23716  rpvmasumlem  23789  eupath2lem3  25100  eupath2  25101  frgrawopreglem2  25166  blocnilem  25836  pjssge0ii  26717  unierri  27139  xlt2addrd  27728  locfinref  27998  esumcst  28211  ballotlem5  28621  itgaddnclem2  30240  pell14qrgt0  30960  monotoddzzfi  31043  rmxypos  31050  rmygeid  31067  stoweidlem18  31966  stoweidlem55  32003  wallispi2lem1  32019  fourierdlem62  32117  fourierdlem103  32158  fourierdlem104  32159  fourierswlem  32179  pgrpgt2nabl  33159  pw2m1lepw2m1  33327
  Copyright terms: Public domain W3C validator