Theorem eqbrtrrd 4117

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  dftpos4  6472  phpm  7095  unsnfidcex  7155  fisseneq  7170  f1finf1o  7189  prmuloclemcalc  7845  mullocprlem  7850  cauappcvgprlemladdfl  7935  caucvgprlemopl  7949  caucvgprprlemloccalc  7964  caucvgprprlemopl  7977  ltadd1sr  8056  suplocsrlem  8088  axarch  8171  axpre-suploclemres  8181  lemulge11  9105  mul2lt0llt0  10057  mul2lt0lgt0  10058  mul2lt0pn  10060  xaddge0  10174  modqmuladdim  10692  ltexp2a  10916  leexp2a  10917  nnlesq  10968  faclbnd6  11069  facavg  11071  fiprsshashgt1  11144  cvg1nlemcxze  11622  resqrexlemover  11650  resqrexlemlo  11653  resqrexlemnmsq  11657  resqrexlemnm  11658  leabs  11714  abs3dif  11745  abs2dif  11746  maxabslemlub  11847  maxltsup  11858  bdtri  11880  xrmaxiflemab  11887  xrbdtri  11916  recn2  11957  imcn2  11958  iserex  11979  summodclem2a  12022  fsumge1  12102  isumrpcl  12135  cvgratnnlemseq  12167  cvgratnnlemsumlt  12169  mertenslemi1  12176  prodmodclem2a  12217  ege2le3  12312  efgt1p2  12336  efgt1p  12337  tanval2ap  12354  tanval3ap  12355  cos12dec  12409  eirraplem  12418  fsumdvds  12483  divalglemnqt  12561  bitsfzo  12596  bitsmod  12597  bitscmp  12599  mulgcd  12667  dvdssqlem  12681  nn0seqcvgd  12693  mulgcddvds  12746  rpdvds  12751  isprm5  12794  pw2dvdseulemle  12819  sqrt2irraplemnn  12831  qden1elz  12857  phimullem  12877  hashgcdlem  12890  hashgcdeq  12892  pceu  12948  pcdvdstr  12980  pockthg  13010  4sqlem11  13054  ennnfonelemex  13115  znrrg  14756  lmcn2  15091  psmetge0  15142  xmetge0  15176  cnopnap  15422  suplociccex  15436  ivthinclemlopn  15447  ivthinclemuopn  15449  hoverb  15459  ivthdichlem  15462  cnplimclemr  15480  limccnp2lem  15487  dveflem  15537  efltlemlt  15585  cosq23lt0  15644  coseq0q4123  15645  cosq34lt1  15661  logdivlti  15692  lgsne0  15857  lgsquadlem1  15896  lgsquadlem2  15897  umgrnloopv  16055  umgredgprv  16056  upgr1een  16065  1hegrvtxdg1fi  16250  apdiff  16780  taupi  16806