Theorem eqbrtrrd 4011

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

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

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 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  dftpos4  6239  phpm  6839  unsnfidcex  6893  fisseneq  6905  f1finf1o  6920  prmuloclemcalc  7514  mullocprlem  7519  cauappcvgprlemladdfl  7604  caucvgprlemopl  7618  caucvgprprlemloccalc  7633  caucvgprprlemopl  7646  ltadd1sr  7725  suplocsrlem  7757  axarch  7840  axpre-suploclemres  7850  lemulge11  8769  mul2lt0llt0  9705  mul2lt0lgt0  9706  mul2lt0pn  9708  xaddge0  9822  modqmuladdim  10310  ltexp2a  10515  leexp2a  10516  nnlesq  10566  faclbnd6  10665  facavg  10667  fiprsshashgt1  10739  cvg1nlemcxze  10933  resqrexlemover  10961  resqrexlemlo  10964  resqrexlemnmsq  10968  resqrexlemnm  10969  leabs  11025  abs3dif  11056  abs2dif  11057  maxabslemlub  11158  maxltsup  11169  bdtri  11190  xrmaxiflemab  11197  xrbdtri  11226  recn2  11267  imcn2  11268  iserex  11289  summodclem2a  11331  fsumge1  11411  isumrpcl  11444  cvgratnnlemseq  11476  cvgratnnlemsumlt  11478  mertenslemi1  11485  prodmodclem2a  11526  ege2le3  11621  efgt1p2  11645  efgt1p  11646  tanval2ap  11663  tanval3ap  11664  cos12dec  11717  eirraplem  11726  divalglemnqt  11866  mulgcd  11958  dvdssqlem  11972  nn0seqcvgd  11982  mulgcddvds  12035  rpdvds  12040  isprm5  12083  pw2dvdseulemle  12108  sqrt2irraplemnn  12120  qden1elz  12146  phimullem  12166  hashgcdlem  12179  hashgcdeq  12180  pceu  12236  pcdvdstr  12267  pockthg  12296  ennnfonelemex  12356  lmcn2  13033  psmetge0  13084  xmetge0  13118  cnopnap  13347  suplociccex  13356  ivthinclemlopn  13367  ivthinclemuopn  13369  cnplimclemr  13391  limccnp2lem  13398  dveflem  13440  efltlemlt  13448  cosq23lt0  13507  coseq0q4123  13508  cosq34lt1  13524  logdivlti  13555  lgsne0  13692  apdiff  14040  taupi  14062