Theorem eqbrtrrd 4005

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

Syntax hints:   -> wi 4   = wceq 1343   class class class wbr 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  dftpos4  6227  phpm  6827  unsnfidcex  6881  fisseneq  6893  f1finf1o  6908  prmuloclemcalc  7502  mullocprlem  7507  cauappcvgprlemladdfl  7592  caucvgprlemopl  7606  caucvgprprlemloccalc  7621  caucvgprprlemopl  7634  ltadd1sr  7713  suplocsrlem  7745  axarch  7828  axpre-suploclemres  7838  lemulge11  8757  mul2lt0llt0  9693  mul2lt0lgt0  9694  mul2lt0pn  9696  xaddge0  9810  modqmuladdim  10298  ltexp2a  10503  leexp2a  10504  nnlesq  10554  faclbnd6  10653  facavg  10655  fiprsshashgt1  10726  cvg1nlemcxze  10920  resqrexlemover  10948  resqrexlemlo  10951  resqrexlemnmsq  10955  resqrexlemnm  10956  leabs  11012  abs3dif  11043  abs2dif  11044  maxabslemlub  11145  maxltsup  11156  bdtri  11177  xrmaxiflemab  11184  xrbdtri  11213  recn2  11254  imcn2  11255  iserex  11276  summodclem2a  11318  fsumge1  11398  isumrpcl  11431  cvgratnnlemseq  11463  cvgratnnlemsumlt  11465  mertenslemi1  11472  prodmodclem2a  11513  ege2le3  11608  efgt1p2  11632  efgt1p  11633  tanval2ap  11650  tanval3ap  11651  cos12dec  11704  eirraplem  11713  divalglemnqt  11853  mulgcd  11945  dvdssqlem  11959  nn0seqcvgd  11969  mulgcddvds  12022  rpdvds  12027  isprm5  12070  pw2dvdseulemle  12095  sqrt2irraplemnn  12107  qden1elz  12133  phimullem  12153  hashgcdlem  12166  hashgcdeq  12167  pceu  12223  pcdvdstr  12254  pockthg  12283  ennnfonelemex  12343  lmcn2  12880  psmetge0  12931  xmetge0  12965  cnopnap  13194  suplociccex  13203  ivthinclemlopn  13214  ivthinclemuopn  13216  cnplimclemr  13238  limccnp2lem  13245  dveflem  13287  efltlemlt  13295  cosq23lt0  13354  coseq0q4123  13355  cosq34lt1  13371  logdivlti  13402  lgsne0  13539  apdiff  13887  taupi  13909