Theorem eqbrtrrd 4149

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 4147	1 |- ( ph -> B R C )

Syntax hints:   -> wi 4   = wceq 1402   class class class wbr 4125

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 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 theorem 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 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  dftpos4  6524  phpm  7157  unsnfidcex  7217  fisseneq  7232  f1finf1o  7254  prmuloclemcalc  7922  mullocprlem  7927  cauappcvgprlemladdfl  8012  caucvgprlemopl  8026  caucvgprprlemloccalc  8041  caucvgprprlemopl  8054  ltadd1sr  8133  suplocsrlem  8165  axarch  8248  axpre-suploclemres  8258  lemulge11  9186  mul2lt0llt0  10141  mul2lt0lgt0  10142  mul2lt0pn  10144  xaddge0  10259  modqmuladdim  10782  ltexp2a  11006  leexp2a  11007  nnlesq  11058  faclbnd6  11160  facavg  11162  bcm1n  11185  fiprsshashgt1  11236  sseqn  11257  sq01  11638  cvg1nlemcxze  11726  resqrexlemover  11754  resqrexlemlo  11757  resqrexlemnmsq  11761  resqrexlemnm  11762  leabs  11818  abs3dif  11849  abs2dif  11850  maxabslemlub  11951  maxltsup  11962  bdtri  11984  xrmaxiflemab  11991  xrbdtri  12020  recn2  12061  imcn2  12062  iserex  12083  summodclem2a  12126  fsumge1  12206  isumrpcl  12239  cvgratnnlemseq  12271  cvgratnnlemsumlt  12273  mertenslemi1  12280  prodmodclem2a  12321  ege2le3  12416  efgt1p2  12440  efgt1p  12441  tanval2ap  12458  tanval3ap  12459  cos12dec  12513  eirraplem  12522  fsumdvds  12587  divalglemnqt  12665  bitsfzo  12700  bitsmod  12701  bitscmp  12703  mulgcd  12771  dvdssqlem  12785  nn0seqcvgd  12797  mulgcddvds  12850  rpdvds  12855  isprm5  12898  pw2dvdseulemle  12923  sqrt2irraplemnn  12935  qden1elz  12961  phimullem  12981  hashgcdlem  12994  hashgcdeq  12996  pceu  13052  pcdvdstr  13084  pockthg  13114  4sqlem11  13158  ennnfonelemex  13283  znrrg  14967  lmcn2  15304  psmetge0  15355  xmetge0  15389  cnopnap  15635  suplociccex  15649  ivthinclemlopn  15660  ivthinclemuopn  15662  hoverb  15672  ivthdichlem  15675  cnplimclemr  15693  limccnp2lem  15700  dveflem  15750  efltlemlt  15798  cosq23lt0  15857  coseq0q4123  15858  cosq34lt1  15874  logdivlti  15905  lgsne0  16071  lgsquadlem1  16110  lgsquadlem2  16111  umgrnloopv  16269  umgredgprv  16270  upgr1een  16279  1hegrvtxdg1fi  16464  apdiff  17002  taupi  17028