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

Theorem syl5breqr 4462
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 2437 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4461 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  r1sdom  8244  alephordilem1  8502  mulge0  10131  xsubge0  11547  xmulgt0  11569  xmulge0  11570  xlemul1a  11574  sqlecan  12378  bernneq  12395  hashge1  12565  hashge2el2dif  12630  cnpart  13282  sqr0lem  13283  bitsfzo  14383  bitsmod  14384  bitsinv1lem  14389  pcge0  14774  prmreclem4  14826  prmreclem5  14827  isabvd  17983  abvtrivd  18003  isnzr2hash  18423  nmolb2d  21650  nmoi  21660  nmoleub  21663  nmo0  21667  ovolge0  22312  itg1ge0a  22546  fta1g  22993  plyrem  23126  taylfval  23179  abelthlem2  23252  sinq12ge0  23328  relogrn  23376  logneg  23402  cxpge0  23493  amgmlem  23780  bposlem5  24079  lgsdir2lem2  24115  rpvmasumlem  24188  eupath2lem3  25552  eupath2  25553  frgrawopreglem2  25618  blocnilem  26290  pjssge0ii  27170  unierri  27592  xlt2addrd  28179  locfinref  28507  esumcst  28723  ballotlem5  29158  poimirlem23  31667  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  itgaddnclem2  31705  pell14qrgt0  35413  monotoddzzfi  35496  rmxypos  35503  rmygeid  35520  stoweidlem18  37447  stoweidlem55  37485  wallispi2lem1  37502  fourierdlem62  37600  fourierdlem103  37641  fourierdlem104  37642  fourierswlem  37662  pgrpgt2nabl  38911  pw2m1lepw2m1  39079
  Copyright terms: Public domain W3C validator