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  7049  ccfunen  7461  prarloclemcalc  7700  ltexprlemopu  7801  recexprlemloc  7829  caucvgprprlemloccalc  7882  suplocsrlem  8006  axpre-suploclemres  8099  mulle0r  9102  lbinfle  9108  divge1  9931  xltnegi  10043  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xposdif  10090  xleaddadd  10095  ubmelm1fzo  10444  zsupssdc  10470  qbtwnrelemcalc  10487  qbtwnxr  10489  ceiqm1l  10545  ceilqm1lt  10546  ceilqle  10548  modqlt  10567  modqeqmodmin  10628  addmodlteq  10632  seqf1oglem1  10753  exp3vallem  10774  bernneq  10894  nn0ltexp2  10943  faclbnd2  10976  ccatsymb  11150  ccatrn  11157  resqrexlemdec  11538  resqrexlemcalc2  11542  resqrexlemglsq  11549  resqrexlemga  11550  abslt  11615  amgm2  11645  icodiamlt  11707  maxabsle  11731  maxltsup  11745  minmax  11757  min1inf  11759  min2inf  11760  bdtrilem  11766  xrmaxltsup  11785  xrmaxaddlem  11787  xrmaxadd  11788  xrminmax  11792  xrmin1inf  11794  xrmin2inf  11795  climconst  11817  serclim0  11832  mulcn2  11839  reccn2ap  11840  iserex  11866  climlec2  11868  iserge0  11870  climcau  11874  climcvg1nlem  11876  fsumabs  11992  iserabs  12002  isumlessdc  12023  divcnv  12024  expcnvre  12030  absgtap  12037  georeclim  12040  cvgratnnlembern  12050  cvgratnnlemsumlt  12055  cvgratnnlemfm  12056  cvgratnnlemrate  12057  mertenslemub  12061  mertenslemi1  12062  prodfclim1  12071  prodfap0  12072  efcvgfsum  12194  eftlub  12217  eflegeo  12228  tanval3ap  12241  tannegap  12255  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  cos01gt0  12290  bitsfzolem  12481  bitsfzo  12482  bitsinv1lem  12488  mulgcd  12553  nnminle  12572  eucalglt  12595  lcmledvds  12608  mulgcddvds  12632  prmind2  12658  isprm5lem  12679  pw2dvdslemn  12703  pw2dvdseulemle  12705  oddpwdclemdvds  12708  sqrt2irrap  12718  divdenle  12735  nonsq  12745  pythagtriplem4  12807  pclem0  12825  pcpremul  12832  pczdvds  12853  pcprmpw2  12872  qexpz  12891  4sqlem10  12926  ennnfonelemkh  12999  prdsbaslemss  13323  triv1nsgd  13771  qusgrp  13785  bl2in  15093  xblcntrps  15103  xblcntr  15104  ssblps  15115  ssbl  15116  blssps  15117  blss  15118  xmetxp  15197  mulc1cncf  15279  cncfmptc  15286  mulcncflem  15297  ivthinclemlopn  15326  ivthinclemuopn  15328  ivthdec  15334  ivthreinc  15335  hovera  15337  hoverlt1  15339  limcimolemlt  15354  cnplimclemle  15358  cnplimclemr  15359  limccnp2lem  15366  dveflem  15416  reeff1olem  15461  reeff1oleme  15462  tangtx  15528  cosq34lt1  15540  logdivlti  15571  cxpap0  15594  rpabscxpbnd  15630  mersenne  15687  lgslem3  15697  gausslemma2dlem1a  15753  lgsquadlem1  15772  lgsquadlem2  15773  2lgslem1c  15785  qdencn  16483  cvgcmp2nlemabs  16488  trilpolemclim  16492  trilpolemisumle  16494  trilpolemeq1  16496  apdifflemf  16502  apdifflemr  16503