Theorem eqbrtrrd 4138

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  dftpos4  6507  phpm  7133  unsnfidcex  7193  fisseneq  7208  f1finf1o  7230  prmuloclemcalc  7896  mullocprlem  7901  cauappcvgprlemladdfl  7986  caucvgprlemopl  8000  caucvgprprlemloccalc  8015  caucvgprprlemopl  8028  ltadd1sr  8107  suplocsrlem  8139  axarch  8222  axpre-suploclemres  8232  lemulge11  9157  mul2lt0llt0  10112  mul2lt0lgt0  10113  mul2lt0pn  10115  xaddge0  10230  modqmuladdim  10753  ltexp2a  10977  leexp2a  10978  nnlesq  11029  faclbnd6  11131  facavg  11133  bcm1n  11156  fiprsshashgt1  11207  sseqn  11228  cvg1nlemcxze  11692  resqrexlemover  11720  resqrexlemlo  11723  resqrexlemnmsq  11727  resqrexlemnm  11728  leabs  11784  abs3dif  11815  abs2dif  11816  maxabslemlub  11917  maxltsup  11928  bdtri  11950  xrmaxiflemab  11957  xrbdtri  11986  recn2  12027  imcn2  12028  iserex  12049  summodclem2a  12092  fsumge1  12172  isumrpcl  12205  cvgratnnlemseq  12237  cvgratnnlemsumlt  12239  mertenslemi1  12246  prodmodclem2a  12287  ege2le3  12382  efgt1p2  12406  efgt1p  12407  tanval2ap  12424  tanval3ap  12425  cos12dec  12479  eirraplem  12488  fsumdvds  12553  divalglemnqt  12631  bitsfzo  12666  bitsmod  12667  bitscmp  12669  mulgcd  12737  dvdssqlem  12751  nn0seqcvgd  12763  mulgcddvds  12816  rpdvds  12821  isprm5  12864  pw2dvdseulemle  12889  sqrt2irraplemnn  12901  qden1elz  12927  phimullem  12947  hashgcdlem  12960  hashgcdeq  12962  pceu  13018  pcdvdstr  13050  pockthg  13080  4sqlem11  13124  ennnfonelemex  13249  znrrg  14934  lmcn2  15271  psmetge0  15322  xmetge0  15356  cnopnap  15602  suplociccex  15616  ivthinclemlopn  15627  ivthinclemuopn  15629  hoverb  15639  ivthdichlem  15642  cnplimclemr  15660  limccnp2lem  15667  dveflem  15717  efltlemlt  15765  cosq23lt0  15824  coseq0q4123  15825  cosq34lt1  15841  logdivlti  15872  lgsne0  16037  lgsquadlem1  16076  lgsquadlem2  16077  umgrnloopv  16235  umgredgprv  16236  upgr1een  16245  1hegrvtxdg1fi  16430  apdiff  16958  taupi  16985