Theorem eqbrtrrd 4083

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  dftpos4  6372  phpm  6988  unsnfidcex  7043  fisseneq  7057  f1finf1o  7075  prmuloclemcalc  7713  mullocprlem  7718  cauappcvgprlemladdfl  7803  caucvgprlemopl  7817  caucvgprprlemloccalc  7832  caucvgprprlemopl  7845  ltadd1sr  7924  suplocsrlem  7956  axarch  8039  axpre-suploclemres  8049  lemulge11  8974  mul2lt0llt0  9918  mul2lt0lgt0  9919  mul2lt0pn  9921  xaddge0  10035  modqmuladdim  10549  ltexp2a  10773  leexp2a  10774  nnlesq  10825  faclbnd6  10926  facavg  10928  fiprsshashgt1  10999  cvg1nlemcxze  11408  resqrexlemover  11436  resqrexlemlo  11439  resqrexlemnmsq  11443  resqrexlemnm  11444  leabs  11500  abs3dif  11531  abs2dif  11532  maxabslemlub  11633  maxltsup  11644  bdtri  11666  xrmaxiflemab  11673  xrbdtri  11702  recn2  11743  imcn2  11744  iserex  11765  summodclem2a  11807  fsumge1  11887  isumrpcl  11920  cvgratnnlemseq  11952  cvgratnnlemsumlt  11954  mertenslemi1  11961  prodmodclem2a  12002  ege2le3  12097  efgt1p2  12121  efgt1p  12122  tanval2ap  12139  tanval3ap  12140  cos12dec  12194  eirraplem  12203  fsumdvds  12268  divalglemnqt  12346  bitsfzo  12381  bitsmod  12382  bitscmp  12384  mulgcd  12452  dvdssqlem  12466  nn0seqcvgd  12478  mulgcddvds  12531  rpdvds  12536  isprm5  12579  pw2dvdseulemle  12604  sqrt2irraplemnn  12616  qden1elz  12642  phimullem  12662  hashgcdlem  12675  hashgcdeq  12677  pceu  12733  pcdvdstr  12765  pockthg  12795  4sqlem11  12839  ennnfonelemex  12900  znrrg  14537  lmcn2  14867  psmetge0  14918  xmetge0  14952  cnopnap  15198  suplociccex  15212  ivthinclemlopn  15223  ivthinclemuopn  15225  hoverb  15235  ivthdichlem  15238  cnplimclemr  15256  limccnp2lem  15263  dveflem  15313  efltlemlt  15361  cosq23lt0  15420  coseq0q4123  15421  cosq34lt1  15437  logdivlti  15468  lgsne0  15630  lgsquadlem1  15669  lgsquadlem2  15670  umgrnloopvv  15825  apdiff  16189  taupi  16214