Theorem eqbrtrrd 4013

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

Syntax hints:   -> wi 4   = wceq 1348   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  dftpos4  6242  phpm  6843  unsnfidcex  6897  fisseneq  6909  f1finf1o  6924  prmuloclemcalc  7527  mullocprlem  7532  cauappcvgprlemladdfl  7617  caucvgprlemopl  7631  caucvgprprlemloccalc  7646  caucvgprprlemopl  7659  ltadd1sr  7738  suplocsrlem  7770  axarch  7853  axpre-suploclemres  7863  lemulge11  8782  mul2lt0llt0  9718  mul2lt0lgt0  9719  mul2lt0pn  9721  xaddge0  9835  modqmuladdim  10323  ltexp2a  10528  leexp2a  10529  nnlesq  10579  faclbnd6  10678  facavg  10680  fiprsshashgt1  10752  cvg1nlemcxze  10946  resqrexlemover  10974  resqrexlemlo  10977  resqrexlemnmsq  10981  resqrexlemnm  10982  leabs  11038  abs3dif  11069  abs2dif  11070  maxabslemlub  11171  maxltsup  11182  bdtri  11203  xrmaxiflemab  11210  xrbdtri  11239  recn2  11280  imcn2  11281  iserex  11302  summodclem2a  11344  fsumge1  11424  isumrpcl  11457  cvgratnnlemseq  11489  cvgratnnlemsumlt  11491  mertenslemi1  11498  prodmodclem2a  11539  ege2le3  11634  efgt1p2  11658  efgt1p  11659  tanval2ap  11676  tanval3ap  11677  cos12dec  11730  eirraplem  11739  divalglemnqt  11879  mulgcd  11971  dvdssqlem  11985  nn0seqcvgd  11995  mulgcddvds  12048  rpdvds  12053  isprm5  12096  pw2dvdseulemle  12121  sqrt2irraplemnn  12133  qden1elz  12159  phimullem  12179  hashgcdlem  12192  hashgcdeq  12193  pceu  12249  pcdvdstr  12280  pockthg  12309  ennnfonelemex  12369  lmcn2  13074  psmetge0  13125  xmetge0  13159  cnopnap  13388  suplociccex  13397  ivthinclemlopn  13408  ivthinclemuopn  13410  cnplimclemr  13432  limccnp2lem  13439  dveflem  13481  efltlemlt  13489  cosq23lt0  13548  coseq0q4123  13549  cosq34lt1  13565  logdivlti  13596  lgsne0  13733  apdiff  14080  taupi  14102