Theorem eqbrtrrd 3947

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

Syntax hints:   -> wi 4   = wceq 1331   class class class wbr 3924

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925

This theorem is referenced by:  dftpos4  6153  phpm  6752  unsnfidcex  6801  fisseneq  6813  f1finf1o  6828  prmuloclemcalc  7366  mullocprlem  7371  cauappcvgprlemladdfl  7456  caucvgprlemopl  7470  caucvgprprlemloccalc  7485  caucvgprprlemopl  7498  ltadd1sr  7577  suplocsrlem  7609  axarch  7692  axpre-suploclemres  7702  lemulge11  8617  mul2lt0llt0  9541  mul2lt0lgt0  9542  mul2lt0pn  9544  xaddge0  9654  modqmuladdim  10133  ltexp2a  10338  leexp2a  10339  nnlesq  10389  faclbnd6  10483  facavg  10485  fiprsshashgt1  10556  cvg1nlemcxze  10747  resqrexlemover  10775  resqrexlemlo  10778  resqrexlemnmsq  10782  resqrexlemnm  10783  leabs  10839  abs3dif  10870  abs2dif  10871  maxabslemlub  10972  maxltsup  10983  bdtri  11004  xrmaxiflemab  11009  xrbdtri  11038  recn2  11079  imcn2  11080  iserex  11101  summodclem2a  11143  fsumge1  11223  isumrpcl  11256  cvgratnnlemseq  11288  cvgratnnlemsumlt  11290  mertenslemi1  11297  ege2le3  11366  efgt1p2  11390  efgt1p  11391  tanval2ap  11409  tanval3ap  11410  cos12dec  11463  eirraplem  11472  divalglemnqt  11606  mulgcd  11693  dvdssqlem  11707  nn0seqcvgd  11711  mulgcddvds  11764  rpdvds  11769  pw2dvdseulemle  11834  sqrt2irraplemnn  11846  qden1elz  11872  phimullem  11890  hashgcdlem  11892  hashgcdeq  11893  ennnfonelemex  11916  lmcn2  12438  psmetge0  12489  xmetge0  12523  cnopnap  12752  suplociccex  12761  ivthinclemlopn  12772  ivthinclemuopn  12774  cnplimclemr  12796  limccnp2lem  12803  dveflem  12844  cosq23lt0  12903  coseq0q4123  12904  cosq34lt1  12920  taupi  13228