Theorem eqbrtrrd 4058

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  dftpos4  6330  phpm  6935  unsnfidcex  6990  fisseneq  7004  f1finf1o  7022  prmuloclemcalc  7649  mullocprlem  7654  cauappcvgprlemladdfl  7739  caucvgprlemopl  7753  caucvgprprlemloccalc  7768  caucvgprprlemopl  7781  ltadd1sr  7860  suplocsrlem  7892  axarch  7975  axpre-suploclemres  7985  lemulge11  8910  mul2lt0llt0  9853  mul2lt0lgt0  9854  mul2lt0pn  9856  xaddge0  9970  modqmuladdim  10476  ltexp2a  10700  leexp2a  10701  nnlesq  10752  faclbnd6  10853  facavg  10855  fiprsshashgt1  10926  cvg1nlemcxze  11164  resqrexlemover  11192  resqrexlemlo  11195  resqrexlemnmsq  11199  resqrexlemnm  11200  leabs  11256  abs3dif  11287  abs2dif  11288  maxabslemlub  11389  maxltsup  11400  bdtri  11422  xrmaxiflemab  11429  xrbdtri  11458  recn2  11499  imcn2  11500  iserex  11521  summodclem2a  11563  fsumge1  11643  isumrpcl  11676  cvgratnnlemseq  11708  cvgratnnlemsumlt  11710  mertenslemi1  11717  prodmodclem2a  11758  ege2le3  11853  efgt1p2  11877  efgt1p  11878  tanval2ap  11895  tanval3ap  11896  cos12dec  11950  eirraplem  11959  fsumdvds  12024  divalglemnqt  12102  bitsfzo  12137  bitsmod  12138  bitscmp  12140  mulgcd  12208  dvdssqlem  12222  nn0seqcvgd  12234  mulgcddvds  12287  rpdvds  12292  isprm5  12335  pw2dvdseulemle  12360  sqrt2irraplemnn  12372  qden1elz  12398  phimullem  12418  hashgcdlem  12431  hashgcdeq  12433  pceu  12489  pcdvdstr  12521  pockthg  12551  4sqlem11  12595  ennnfonelemex  12656  znrrg  14292  lmcn2  14600  psmetge0  14651  xmetge0  14685  cnopnap  14931  suplociccex  14945  ivthinclemlopn  14956  ivthinclemuopn  14958  hoverb  14968  ivthdichlem  14971  cnplimclemr  14989  limccnp2lem  14996  dveflem  15046  efltlemlt  15094  cosq23lt0  15153  coseq0q4123  15154  cosq34lt1  15170  logdivlti  15201  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  apdiff  15779  taupi  15804