Theorem eqbrtrd 4081

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 4069	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  eqbrtrrd  4083  dif1en  7002  ccfunen  7411  prarloclemcalc  7650  ltexprlemopu  7751  recexprlemloc  7779  caucvgprprlemloccalc  7832  suplocsrlem  7956  axpre-suploclemres  8049  mulle0r  9052  lbinfle  9058  divge1  9880  xltnegi  9992  xleadd1a  10030  xltadd1  10033  xlt2add  10037  xposdif  10039  xleaddadd  10044  ubmelm1fzo  10392  zsupssdc  10418  qbtwnrelemcalc  10435  qbtwnxr  10437  ceiqm1l  10493  ceilqm1lt  10494  ceilqle  10496  modqlt  10515  modqeqmodmin  10576  addmodlteq  10580  seqf1oglem1  10701  exp3vallem  10722  bernneq  10842  nn0ltexp2  10891  faclbnd2  10924  ccatsymb  11096  ccatrn  11103  resqrexlemdec  11437  resqrexlemcalc2  11441  resqrexlemglsq  11448  resqrexlemga  11449  abslt  11514  amgm2  11544  icodiamlt  11606  maxabsle  11630  maxltsup  11644  minmax  11656  min1inf  11658  min2inf  11659  bdtrilem  11665  xrmaxltsup  11684  xrmaxaddlem  11686  xrmaxadd  11687  xrminmax  11691  xrmin1inf  11693  xrmin2inf  11694  climconst  11716  serclim0  11731  mulcn2  11738  reccn2ap  11739  iserex  11765  climlec2  11767  iserge0  11769  climcau  11773  climcvg1nlem  11775  fsumabs  11891  iserabs  11901  isumlessdc  11922  divcnv  11923  expcnvre  11929  absgtap  11936  georeclim  11939  cvgratnnlembern  11949  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  mertenslemub  11960  mertenslemi1  11961  prodfclim1  11970  prodfap0  11971  efcvgfsum  12093  eftlub  12116  eflegeo  12127  tanval3ap  12140  tannegap  12154  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos01gt0  12189  bitsfzolem  12380  bitsfzo  12381  bitsinv1lem  12387  mulgcd  12452  nnminle  12471  eucalglt  12494  lcmledvds  12507  mulgcddvds  12531  prmind2  12557  isprm5lem  12578  pw2dvdslemn  12602  pw2dvdseulemle  12604  oddpwdclemdvds  12607  sqrt2irrap  12617  divdenle  12634  nonsq  12644  pythagtriplem4  12706  pclem0  12724  pcpremul  12731  pczdvds  12752  pcprmpw2  12771  qexpz  12790  4sqlem10  12825  ennnfonelemkh  12898  prdsbaslemss  13221  triv1nsgd  13669  qusgrp  13683  bl2in  14990  xblcntrps  15000  xblcntr  15001  ssblps  15012  ssbl  15013  blssps  15014  blss  15015  xmetxp  15094  mulc1cncf  15176  cncfmptc  15183  mulcncflem  15194  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthdec  15231  ivthreinc  15232  hovera  15234  hoverlt1  15236  limcimolemlt  15251  cnplimclemle  15255  cnplimclemr  15256  limccnp2lem  15263  dveflem  15313  reeff1olem  15358  reeff1oleme  15359  tangtx  15425  cosq34lt1  15437  logdivlti  15468  cxpap0  15491  rpabscxpbnd  15527  mersenne  15584  lgslem3  15594  gausslemma2dlem1a  15650  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1c  15682  qdencn  16168  cvgcmp2nlemabs  16173  trilpolemclim  16177  trilpolemisumle  16179  trilpolemeq1  16181  apdifflemf  16187  apdifflemr  16188