Theorem eqbrtrrd 3873

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

Syntax hints:   -> wi 4   = wceq 1290   class class class wbr 3851

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-un 3004  df-sn 3456  df-pr 3457  df-op 3459  df-br 3852

This theorem is referenced by:  dftpos4  6042  phpm  6635  unsnfidcex  6684  fisseneq  6696  f1finf1o  6710  prmuloclemcalc  7178  mullocprlem  7183  cauappcvgprlemladdfl  7268  caucvgprlemopl  7282  caucvgprprlemloccalc  7297  caucvgprprlemopl  7310  ltadd1sr  7376  axarch  7480  lemulge11  8381  modqmuladdim  9828  ltexp2a  10061  leexp2a  10062  nnlesq  10112  faclbnd6  10206  facavg  10208  fiprsshashgt1  10279  cvg1nlemcxze  10469  resqrexlemover  10497  resqrexlemlo  10500  resqrexlemnmsq  10504  resqrexlemnm  10505  leabs  10561  abs3dif  10592  abs2dif  10593  maxabslemlub  10694  maxltsup  10705  recn2  10759  imcn2  10760  iserex  10781  isermulc2  10783  isummolem2a  10825  isummulc2  10874  fsumge1  10909  isumrpcl  10942  cvgratnnlemseq  10974  cvgratnnlemsumlt  10976  mertenslemi1  10983  ege2le3  11015  efgt1p2  11039  efgt1p  11040  tanval2ap  11058  tanval3ap  11059  eirraplem  11118  divalglemnqt  11252  mulgcd  11337  dvdssqlem  11351  nn0seqcvgd  11355  mulgcddvds  11408  rpdvds  11413  pw2dvdseulemle  11477  sqrt2irraplemnn  11489  qden1elz  11515  phimullem  11533  hashgcdlem  11535  hashgcdeq  11536