Theorem eqbrtrrd 4029

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

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4005

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  dftpos4  6266  phpm  6867  unsnfidcex  6921  fisseneq  6933  f1finf1o  6948  prmuloclemcalc  7566  mullocprlem  7571  cauappcvgprlemladdfl  7656  caucvgprlemopl  7670  caucvgprprlemloccalc  7685  caucvgprprlemopl  7698  ltadd1sr  7777  suplocsrlem  7809  axarch  7892  axpre-suploclemres  7902  lemulge11  8825  mul2lt0llt0  9763  mul2lt0lgt0  9764  mul2lt0pn  9766  xaddge0  9880  modqmuladdim  10369  ltexp2a  10574  leexp2a  10575  nnlesq  10626  faclbnd6  10726  facavg  10728  fiprsshashgt1  10799  cvg1nlemcxze  10993  resqrexlemover  11021  resqrexlemlo  11024  resqrexlemnmsq  11028  resqrexlemnm  11029  leabs  11085  abs3dif  11116  abs2dif  11117  maxabslemlub  11218  maxltsup  11229  bdtri  11250  xrmaxiflemab  11257  xrbdtri  11286  recn2  11327  imcn2  11328  iserex  11349  summodclem2a  11391  fsumge1  11471  isumrpcl  11504  cvgratnnlemseq  11536  cvgratnnlemsumlt  11538  mertenslemi1  11545  prodmodclem2a  11586  ege2le3  11681  efgt1p2  11705  efgt1p  11706  tanval2ap  11723  tanval3ap  11724  cos12dec  11777  eirraplem  11786  divalglemnqt  11927  mulgcd  12019  dvdssqlem  12033  nn0seqcvgd  12043  mulgcddvds  12096  rpdvds  12101  isprm5  12144  pw2dvdseulemle  12169  sqrt2irraplemnn  12181  qden1elz  12207  phimullem  12227  hashgcdlem  12240  hashgcdeq  12241  pceu  12297  pcdvdstr  12328  pockthg  12357  ennnfonelemex  12417  lmcn2  13865  psmetge0  13916  xmetge0  13950  cnopnap  14179  suplociccex  14188  ivthinclemlopn  14199  ivthinclemuopn  14201  cnplimclemr  14223  limccnp2lem  14230  dveflem  14272  efltlemlt  14280  cosq23lt0  14339  coseq0q4123  14340  cosq34lt1  14356  logdivlti  14387  lgsne0  14524  apdiff  14881  taupi  14906