Theorem syl5breqr 4691

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

Step	Hyp	Ref	Expression
1		syl5breqr.1	. 2 |- A R B
2		syl5breqr.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2628	. 2 |- ( ph -> B = C )
4	1, 3	syl5breq 4690	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  r1sdom  8637  alephordilem1  8896  mulge0  10546  xsubge0  12091  xmulgt0  12113  xmulge0  12114  xlemul1a  12118  sqlecan  12971  bernneq  12990  hashge1  13178  hashge2el2dif  13262  cnpart  13980  sqr0lem  13981  bitsfzo  15157  bitsmod  15158  bitsinv1lem  15163  pcge0  15566  prmreclem4  15623  prmreclem5  15624  isabvd  18820  abvtrivd  18840  isnzr2hash  19264  nmolb2d  22522  nmoi  22532  nmoleub  22535  nmo0  22539  ovolge0  23249  itg1ge0a  23478  fta1g  23927  plyrem  24060  taylfval  24113  abelthlem2  24186  sinq12ge0  24260  relogrn  24308  logneg  24334  cxpge0  24429  amgmlem  24716  bposlem5  25013  lgsdir2lem2  25051  2lgsoddprmlem3  25139  rpvmasumlem  25176  eupth2lem3lem3  27090  eupth2lemb  27097  blocnilem  27659  pjssge0ii  28541  unierri  28963  xlt2addrd  29523  locfinref  29908  esumcst  30125  ballotlem5  30561  poimirlem23  33432  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  itgaddnclem2  33469  pell14qrgt0  37423  monotoddzzfi  37507  rmxypos  37514  rmygeid  37531  stoweidlem18  40235  stoweidlem55  40272  wallispi2lem1  40288  fourierdlem62  40385  fourierdlem103  40426  fourierdlem104  40427  fourierswlem  40447  pgrpgt2nabl  42147  pw2m1lepw2m1  42310  amgmwlem  42548