Theorem eqbrtrd 4105

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	|- ( ph -> A = B )
eqbrtrd.2	|- ( ph -> B R C )

Assertion

Ref	Expression
eqbrtrd	|- ( ph -> A R C )

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- ( ph -> B R C )
2		eqbrtrd.1	. . 3 |- ( ph -> A = B )
3	2	breq1d 4093	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A 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:  eqbrtrrd  4107  dif1en  7041  ccfunen  7450  prarloclemcalc  7689  ltexprlemopu  7790  recexprlemloc  7818  caucvgprprlemloccalc  7871  suplocsrlem  7995  axpre-suploclemres  8088  mulle0r  9091  lbinfle  9097  divge1  9919  xltnegi  10031  xleadd1a  10069  xltadd1  10072  xlt2add  10076  xposdif  10078  xleaddadd  10083  ubmelm1fzo  10432  zsupssdc  10458  qbtwnrelemcalc  10475  qbtwnxr  10477  ceiqm1l  10533  ceilqm1lt  10534  ceilqle  10536  modqlt  10555  modqeqmodmin  10616  addmodlteq  10620  seqf1oglem1  10741  exp3vallem  10762  bernneq  10882  nn0ltexp2  10931  faclbnd2  10964  ccatsymb  11137  ccatrn  11144  resqrexlemdec  11522  resqrexlemcalc2  11526  resqrexlemglsq  11533  resqrexlemga  11534  abslt  11599  amgm2  11629  icodiamlt  11691  maxabsle  11715  maxltsup  11729  minmax  11741  min1inf  11743  min2inf  11744  bdtrilem  11750  xrmaxltsup  11769  xrmaxaddlem  11771  xrmaxadd  11772  xrminmax  11776  xrmin1inf  11778  xrmin2inf  11779  climconst  11801  serclim0  11816  mulcn2  11823  reccn2ap  11824  iserex  11850  climlec2  11852  iserge0  11854  climcau  11858  climcvg1nlem  11860  fsumabs  11976  iserabs  11986  isumlessdc  12007  divcnv  12008  expcnvre  12014  absgtap  12021  georeclim  12024  cvgratnnlembern  12034  cvgratnnlemsumlt  12039  cvgratnnlemfm  12040  cvgratnnlemrate  12041  mertenslemub  12045  mertenslemi1  12046  prodfclim1  12055  prodfap0  12056  efcvgfsum  12178  eftlub  12201  eflegeo  12212  tanval3ap  12225  tannegap  12239  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos01gt0  12274  bitsfzolem  12465  bitsfzo  12466  bitsinv1lem  12472  mulgcd  12537  nnminle  12556  eucalglt  12579  lcmledvds  12592  mulgcddvds  12616  prmind2  12642  isprm5lem  12663  pw2dvdslemn  12687  pw2dvdseulemle  12689  oddpwdclemdvds  12692  sqrt2irrap  12702  divdenle  12719  nonsq  12729  pythagtriplem4  12791  pclem0  12809  pcpremul  12816  pczdvds  12837  pcprmpw2  12856  qexpz  12875  4sqlem10  12910  ennnfonelemkh  12983  prdsbaslemss  13307  triv1nsgd  13755  qusgrp  13769  bl2in  15077  xblcntrps  15087  xblcntr  15088  ssblps  15099  ssbl  15100  blssps  15101  blss  15102  xmetxp  15181  mulc1cncf  15263  cncfmptc  15270  mulcncflem  15281  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdec  15318  ivthreinc  15319  hovera  15321  hoverlt1  15323  limcimolemlt  15338  cnplimclemle  15342  cnplimclemr  15343  limccnp2lem  15350  dveflem  15400  reeff1olem  15445  reeff1oleme  15446  tangtx  15512  cosq34lt1  15524  logdivlti  15555  cxpap0  15578  rpabscxpbnd  15614  mersenne  15671  lgslem3  15681  gausslemma2dlem1a  15737  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem1c  15769  qdencn  16395  cvgcmp2nlemabs  16400  trilpolemclim  16404  trilpolemisumle  16406  trilpolemeq1  16408  apdifflemf  16414  apdifflemr  16415