Theorem eqbrtrrd 4154

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  dftpos4  6534  phpm  7167  unsnfidcex  7227  fisseneq  7242  f1finf1o  7264  prmuloclemcalc  7932  mullocprlem  7937  cauappcvgprlemladdfl  8022  caucvgprlemopl  8036  caucvgprprlemloccalc  8051  caucvgprprlemopl  8064  ltadd1sr  8143  suplocsrlem  8175  axarch  8258  axpre-suploclemres  8268  lemulge11  9198  mul2lt0llt0  10172  mul2lt0lgt0  10173  mul2lt0pn  10175  xaddge0  10290  modqmuladdim  10817  ltexp2a  11041  leexp2a  11042  nnlesq  11093  faclbnd6  11196  facavg  11198  bcm1n  11221  fiprsshashgt1  11272  sseqn  11293  sq01  11674  cvg1nlemcxze  11762  resqrexlemover  11790  resqrexlemlo  11793  resqrexlemnmsq  11797  resqrexlemnm  11798  leabs  11854  abs3dif  11886  abs2dif  11887  maxabslemlub  11988  maxltsup  11999  bdtri  12022  xrmaxiflemab  12029  xrbdtri  12058  recn2  12099  imcn2  12100  iserex  12121  summodclem2a  12164  fsumge1  12244  isumrpcl  12277  cvgratnnlemseq  12309  cvgratnnlemsumlt  12311  mertenslemi1  12318  prodmodclem2a  12359  ege2le3  12454  efgt1p2  12478  efgt1p  12479  tanval2ap  12496  tanval3ap  12497  cos12dec  12551  eirraplem  12560  fsumdvds  12625  divalglemnqt  12703  bitsfzo  12738  bitsmod  12739  bitscmp  12741  mulgcd  12809  dvdssqlem  12823  nn0seqcvgd  12835  mulgcddvds  12888  rpdvds  12893  isprm5  12937  pwbdvdseulemle  12962  sqrt2irraplemnn  12975  qden1elz  13001  phimullem  13023  hashgcdlem  13036  hashgcdeq  13038  pceu  13094  pcdvdstr  13126  pockthg  13156  4sqlem11  13200  ennnfonelemex  13354  znrrg  15044  lmcn2  15430  psmetge0  15481  xmetge0  15515  cnopnap  15761  suplociccex  15775  ivthinclemlopn  15786  ivthinclemuopn  15788  hoverb  15798  ivthdichlem  15801  cnplimclemr  15819  limccnp2lem  15826  dveflem  15876  efltlemlt  15924  cosq23lt0  15984  coseq0q4123  15985  cosq34lt1  16001  logdivlti  16033  logdivlt  16046  ppiqltx  16183  bcmono  16202  bposlem2  16210  bposlem5  16213  lgsne0  16255  lgsquadlem1  16294  lgsquadlem2  16295  umgrnloopv  16453  umgredgprv  16454  upgr1een  16463  1hegrvtxdg1fi  16648  apdiff  17195  taupi  17221