Theorem eqbrtrrd 4107

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

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  dftpos4  6415  phpm  7035  unsnfidcex  7093  fisseneq  7107  f1finf1o  7125  prmuloclemcalc  7763  mullocprlem  7768  cauappcvgprlemladdfl  7853  caucvgprlemopl  7867  caucvgprprlemloccalc  7882  caucvgprprlemopl  7895  ltadd1sr  7974  suplocsrlem  8006  axarch  8089  axpre-suploclemres  8099  lemulge11  9024  mul2lt0llt0  9969  mul2lt0lgt0  9970  mul2lt0pn  9972  xaddge0  10086  modqmuladdim  10601  ltexp2a  10825  leexp2a  10826  nnlesq  10877  faclbnd6  10978  facavg  10980  fiprsshashgt1  11052  cvg1nlemcxze  11509  resqrexlemover  11537  resqrexlemlo  11540  resqrexlemnmsq  11544  resqrexlemnm  11545  leabs  11601  abs3dif  11632  abs2dif  11633  maxabslemlub  11734  maxltsup  11745  bdtri  11767  xrmaxiflemab  11774  xrbdtri  11803  recn2  11844  imcn2  11845  iserex  11866  summodclem2a  11908  fsumge1  11988  isumrpcl  12021  cvgratnnlemseq  12053  cvgratnnlemsumlt  12055  mertenslemi1  12062  prodmodclem2a  12103  ege2le3  12198  efgt1p2  12222  efgt1p  12223  tanval2ap  12240  tanval3ap  12241  cos12dec  12295  eirraplem  12304  fsumdvds  12369  divalglemnqt  12447  bitsfzo  12482  bitsmod  12483  bitscmp  12485  mulgcd  12553  dvdssqlem  12567  nn0seqcvgd  12579  mulgcddvds  12632  rpdvds  12637  isprm5  12680  pw2dvdseulemle  12705  sqrt2irraplemnn  12717  qden1elz  12743  phimullem  12763  hashgcdlem  12776  hashgcdeq  12778  pceu  12834  pcdvdstr  12866  pockthg  12896  4sqlem11  12940  ennnfonelemex  13001  znrrg  14640  lmcn2  14970  psmetge0  15021  xmetge0  15055  cnopnap  15301  suplociccex  15315  ivthinclemlopn  15326  ivthinclemuopn  15328  hoverb  15338  ivthdichlem  15341  cnplimclemr  15359  limccnp2lem  15366  dveflem  15416  efltlemlt  15464  cosq23lt0  15523  coseq0q4123  15524  cosq34lt1  15540  logdivlti  15571  lgsne0  15733  lgsquadlem1  15772  lgsquadlem2  15773  umgrnloopv  15930  umgredgprv  15931  apdiff  16504  taupi  16529