Theorem eqbrtrd 4056

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

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  eqbrtrrd  4058  dif1en  6949  ccfunen  7347  prarloclemcalc  7586  ltexprlemopu  7687  recexprlemloc  7715  caucvgprprlemloccalc  7768  suplocsrlem  7892  axpre-suploclemres  7985  mulle0r  8988  lbinfle  8994  divge1  9815  xltnegi  9927  xleadd1a  9965  xltadd1  9968  xlt2add  9972  xposdif  9974  xleaddadd  9979  ubmelm1fzo  10319  zsupssdc  10345  qbtwnrelemcalc  10362  qbtwnxr  10364  ceiqm1l  10420  ceilqm1lt  10421  ceilqle  10423  modqlt  10442  modqeqmodmin  10503  addmodlteq  10507  seqf1oglem1  10628  exp3vallem  10649  bernneq  10769  nn0ltexp2  10818  faclbnd2  10851  resqrexlemdec  11193  resqrexlemcalc2  11197  resqrexlemglsq  11204  resqrexlemga  11205  abslt  11270  amgm2  11300  icodiamlt  11362  maxabsle  11386  maxltsup  11400  minmax  11412  min1inf  11414  min2inf  11415  bdtrilem  11421  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  xrminmax  11447  xrmin1inf  11449  xrmin2inf  11450  climconst  11472  serclim0  11487  mulcn2  11494  reccn2ap  11495  iserex  11521  climlec2  11523  iserge0  11525  climcau  11529  climcvg1nlem  11531  fsumabs  11647  iserabs  11657  isumlessdc  11678  divcnv  11679  expcnvre  11685  absgtap  11692  georeclim  11695  cvgratnnlembern  11705  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratnnlemrate  11712  mertenslemub  11716  mertenslemi1  11717  prodfclim1  11726  prodfap0  11727  efcvgfsum  11849  eftlub  11872  eflegeo  11883  tanval3ap  11896  tannegap  11910  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos01gt0  11945  bitsfzolem  12136  bitsfzo  12137  bitsinv1lem  12143  mulgcd  12208  nnminle  12227  eucalglt  12250  lcmledvds  12263  mulgcddvds  12287  prmind2  12313  isprm5lem  12334  pw2dvdslemn  12358  pw2dvdseulemle  12360  oddpwdclemdvds  12363  sqrt2irrap  12373  divdenle  12390  nonsq  12400  pythagtriplem4  12462  pclem0  12480  pcpremul  12487  pczdvds  12508  pcprmpw2  12527  qexpz  12546  4sqlem10  12581  ennnfonelemkh  12654  prdsbaslemss  12976  triv1nsgd  13424  qusgrp  13438  bl2in  14723  xblcntrps  14733  xblcntr  14734  ssblps  14745  ssbl  14746  blssps  14747  blss  14748  xmetxp  14827  mulc1cncf  14909  cncfmptc  14916  mulcncflem  14927  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdec  14964  ivthreinc  14965  hovera  14967  hoverlt1  14969  limcimolemlt  14984  cnplimclemle  14988  cnplimclemr  14989  limccnp2lem  14996  dveflem  15046  reeff1olem  15091  reeff1oleme  15092  tangtx  15158  cosq34lt1  15170  logdivlti  15201  cxpap0  15224  rpabscxpbnd  15260  mersenne  15317  lgslem3  15327  gausslemma2dlem1a  15383  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1c  15415  qdencn  15758  cvgcmp2nlemabs  15763  trilpolemclim  15767  trilpolemisumle  15769  trilpolemeq1  15771  apdifflemf  15777  apdifflemr  15778