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

Theorem syl5breqr 4473
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 2451 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4472 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  r1sdom  8195  alephordilem1  8457  mulge0  10077  xsubge0  11464  xmulgt0  11486  xmulge0  11487  xlemul1a  11491  sqlecan  12256  bernneq  12274  hashge1  12439  hashge2el2dif  12503  cnpart  13055  sqr0lem  13056  bitsfzo  14067  bitsmod  14068  bitsinv1lem  14073  pcge0  14367  prmreclem4  14419  prmreclem5  14420  isabvd  17448  abvtrivd  17468  isnzr2hash  17891  nmolb2d  21203  nmoi  21213  nmoleub  21216  nmo0  21220  ovolge0  21870  itg1ge0a  22096  fta1g  22546  plyrem  22679  taylfval  22732  abelthlem2  22805  sinq12ge0  22879  relogrn  22927  logneg  22950  cxpge0  23042  amgmlem  23297  bposlem5  23541  lgsdir2lem2  23577  rpvmasumlem  23650  eupath2lem3  24957  eupath2  24958  frgrawopreglem2  25023  blocnilem  25697  pjssge0ii  26578  unierri  27001  xlt2addrd  27556  locfinref  27822  esumcst  28049  ballotlem5  28416  itgaddnclem2  30050  pell14qrgt0  30771  monotoddzzfi  30854  rmxypos  30861  rmygeid  30878  stoweidlem18  31754  stoweidlem55  31791  wallispi2lem1  31807  fourierdlem62  31905  fourierdlem103  31946  fourierdlem104  31947  fourierswlem  31967  pgrpgt2nabl  32827
  Copyright terms: Public domain W3C validator