Theorem eqbrtrrd 4107

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

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  dftpos4  6409  phpm  7027  unsnfidcex  7082  fisseneq  7096  f1finf1o  7114  prmuloclemcalc  7752  mullocprlem  7757  cauappcvgprlemladdfl  7842  caucvgprlemopl  7856  caucvgprprlemloccalc  7871  caucvgprprlemopl  7884  ltadd1sr  7963  suplocsrlem  7995  axarch  8078  axpre-suploclemres  8088  lemulge11  9013  mul2lt0llt0  9957  mul2lt0lgt0  9958  mul2lt0pn  9960  xaddge0  10074  modqmuladdim  10589  ltexp2a  10813  leexp2a  10814  nnlesq  10865  faclbnd6  10966  facavg  10968  fiprsshashgt1  11039  cvg1nlemcxze  11493  resqrexlemover  11521  resqrexlemlo  11524  resqrexlemnmsq  11528  resqrexlemnm  11529  leabs  11585  abs3dif  11616  abs2dif  11617  maxabslemlub  11718  maxltsup  11729  bdtri  11751  xrmaxiflemab  11758  xrbdtri  11787  recn2  11828  imcn2  11829  iserex  11850  summodclem2a  11892  fsumge1  11972  isumrpcl  12005  cvgratnnlemseq  12037  cvgratnnlemsumlt  12039  mertenslemi1  12046  prodmodclem2a  12087  ege2le3  12182  efgt1p2  12206  efgt1p  12207  tanval2ap  12224  tanval3ap  12225  cos12dec  12279  eirraplem  12288  fsumdvds  12353  divalglemnqt  12431  bitsfzo  12466  bitsmod  12467  bitscmp  12469  mulgcd  12537  dvdssqlem  12551  nn0seqcvgd  12563  mulgcddvds  12616  rpdvds  12621  isprm5  12664  pw2dvdseulemle  12689  sqrt2irraplemnn  12701  qden1elz  12727  phimullem  12747  hashgcdlem  12760  hashgcdeq  12762  pceu  12818  pcdvdstr  12850  pockthg  12880  4sqlem11  12924  ennnfonelemex  12985  znrrg  14624  lmcn2  14954  psmetge0  15005  xmetge0  15039  cnopnap  15285  suplociccex  15299  ivthinclemlopn  15310  ivthinclemuopn  15312  hoverb  15322  ivthdichlem  15325  cnplimclemr  15343  limccnp2lem  15350  dveflem  15400  efltlemlt  15448  cosq23lt0  15507  coseq0q4123  15508  cosq34lt1  15524  logdivlti  15555  lgsne0  15717  lgsquadlem1  15756  lgsquadlem2  15757  umgrnloopv  15914  umgredgprv  15915  apdiff  16416  taupi  16441