Theorem eqbrtrrd 4069

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrrd.1	|- ( ph -> A = B )
eqbrtrrd.2	|- ( ph -> A R C )

Assertion

Ref	Expression
eqbrtrrd	|- ( ph -> B R C )

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2211	. 2 |- ( ph -> B = A )
3		eqbrtrrd.2	. 2 |- ( ph -> A R C )
4	2, 3	eqbrtrd 4067	1 |- ( ph -> B R C )

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  dftpos4  6351  phpm  6964  unsnfidcex  7019  fisseneq  7033  f1finf1o  7051  prmuloclemcalc  7680  mullocprlem  7685  cauappcvgprlemladdfl  7770  caucvgprlemopl  7784  caucvgprprlemloccalc  7799  caucvgprprlemopl  7812  ltadd1sr  7891  suplocsrlem  7923  axarch  8006  axpre-suploclemres  8016  lemulge11  8941  mul2lt0llt0  9885  mul2lt0lgt0  9886  mul2lt0pn  9888  xaddge0  10002  modqmuladdim  10514  ltexp2a  10738  leexp2a  10739  nnlesq  10790  faclbnd6  10891  facavg  10893  fiprsshashgt1  10964  cvg1nlemcxze  11326  resqrexlemover  11354  resqrexlemlo  11357  resqrexlemnmsq  11361  resqrexlemnm  11362  leabs  11418  abs3dif  11449  abs2dif  11450  maxabslemlub  11551  maxltsup  11562  bdtri  11584  xrmaxiflemab  11591  xrbdtri  11620  recn2  11661  imcn2  11662  iserex  11683  summodclem2a  11725  fsumge1  11805  isumrpcl  11838  cvgratnnlemseq  11870  cvgratnnlemsumlt  11872  mertenslemi1  11879  prodmodclem2a  11920  ege2le3  12015  efgt1p2  12039  efgt1p  12040  tanval2ap  12057  tanval3ap  12058  cos12dec  12112  eirraplem  12121  fsumdvds  12186  divalglemnqt  12264  bitsfzo  12299  bitsmod  12300  bitscmp  12302  mulgcd  12370  dvdssqlem  12384  nn0seqcvgd  12396  mulgcddvds  12449  rpdvds  12454  isprm5  12497  pw2dvdseulemle  12522  sqrt2irraplemnn  12534  qden1elz  12560  phimullem  12580  hashgcdlem  12593  hashgcdeq  12595  pceu  12651  pcdvdstr  12683  pockthg  12713  4sqlem11  12757  ennnfonelemex  12818  znrrg  14455  lmcn2  14785  psmetge0  14836  xmetge0  14870  cnopnap  15116  suplociccex  15130  ivthinclemlopn  15141  ivthinclemuopn  15143  hoverb  15153  ivthdichlem  15156  cnplimclemr  15174  limccnp2lem  15181  dveflem  15231  efltlemlt  15279  cosq23lt0  15338  coseq0q4123  15339  cosq34lt1  15355  logdivlti  15386  lgsne0  15548  lgsquadlem1  15587  lgsquadlem2  15588  apdiff  16024  taupi  16049