Theorem eqbrtrrd 4042

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 2195	. 2 |- ( ph -> B = A )
3		eqbrtrrd.2	. 2 |- ( ph -> A R C )
4	2, 3	eqbrtrd 4040	1 |- ( ph -> B R C )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4018

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  dftpos4  6283  phpm  6888  unsnfidcex  6943  fisseneq  6955  f1finf1o  6971  prmuloclemcalc  7589  mullocprlem  7594  cauappcvgprlemladdfl  7679  caucvgprlemopl  7693  caucvgprprlemloccalc  7708  caucvgprprlemopl  7721  ltadd1sr  7800  suplocsrlem  7832  axarch  7915  axpre-suploclemres  7925  lemulge11  8848  mul2lt0llt0  9786  mul2lt0lgt0  9787  mul2lt0pn  9789  xaddge0  9903  modqmuladdim  10393  ltexp2a  10598  leexp2a  10599  nnlesq  10650  faclbnd6  10751  facavg  10753  fiprsshashgt1  10824  cvg1nlemcxze  11018  resqrexlemover  11046  resqrexlemlo  11049  resqrexlemnmsq  11053  resqrexlemnm  11054  leabs  11110  abs3dif  11141  abs2dif  11142  maxabslemlub  11243  maxltsup  11254  bdtri  11275  xrmaxiflemab  11282  xrbdtri  11311  recn2  11352  imcn2  11353  iserex  11374  summodclem2a  11416  fsumge1  11496  isumrpcl  11529  cvgratnnlemseq  11561  cvgratnnlemsumlt  11563  mertenslemi1  11570  prodmodclem2a  11611  ege2le3  11706  efgt1p2  11730  efgt1p  11731  tanval2ap  11748  tanval3ap  11749  cos12dec  11802  eirraplem  11811  divalglemnqt  11952  mulgcd  12044  dvdssqlem  12058  nn0seqcvgd  12068  mulgcddvds  12121  rpdvds  12126  isprm5  12169  pw2dvdseulemle  12194  sqrt2irraplemnn  12206  qden1elz  12232  phimullem  12252  hashgcdlem  12265  hashgcdeq  12266  pceu  12322  pcdvdstr  12354  pockthg  12384  4sqlem11  12428  ennnfonelemex  12460  lmcn2  14217  psmetge0  14268  xmetge0  14302  cnopnap  14531  suplociccex  14540  ivthinclemlopn  14551  ivthinclemuopn  14553  cnplimclemr  14575  limccnp2lem  14582  dveflem  14624  efltlemlt  14632  cosq23lt0  14691  coseq0q4123  14692  cosq34lt1  14708  logdivlti  14739  lgsne0  14876  apdiff  15234  taupi  15259