Theorem eqbrtrd 4147

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

Syntax hints:   -> wi 4   = wceq 1402   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  eqbrtrrd  4149  dif1en  7173  ccfunen  7620  prarloclemcalc  7859  ltexprlemopu  7960  recexprlemloc  7988  caucvgprprlemloccalc  8041  suplocsrlem  8165  axpre-suploclemres  8258  mulle0r  9264  lbinfle  9270  divge1  10103  ltesubnnd  10149  xltnegi  10216  xleadd1a  10254  xltadd1  10257  xlt2add  10261  xposdif  10263  xleaddadd  10268  lincmble  10385  ubmelm1fzo  10622  infssfzledc  10648  zsupssdc  10651  qbtwnrelemcalc  10668  qbtwnxr  10670  ceiqm1l  10726  ceilqm1lt  10727  ceilqle  10729  modqlt  10748  modqeqmodmin  10809  addmodlteq  10813  seqf1oglem1  10934  exp3vallem  10955  bernneq  11076  nn0ltexp2  11125  faclbnd2  11158  sshashneg  11259  ccatsymb  11348  ccatrn  11355  sq01  11638  resqrexlemdec  11755  resqrexlemcalc2  11759  resqrexlemglsq  11766  resqrexlemga  11767  abslt  11832  amgm2  11862  icodiamlt  11924  maxabsle  11948  maxltsup  11962  minmax  11974  min1inf  11976  min2inf  11977  bdtrilem  11983  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  xrminmax  12009  xrmin1inf  12011  xrmin2inf  12012  climconst  12034  serclim0  12049  mulcn2  12056  reccn2ap  12057  iserex  12083  climlec2  12085  iserge0  12087  climcau  12091  climcvg1nlem  12093  fsumabs  12210  iserabs  12220  isumlessdc  12241  divcnv  12242  expcnvre  12248  absgtap  12255  georeclim  12258  cvgratnnlembern  12268  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratnnlemrate  12275  mertenslemub  12279  mertenslemi1  12280  prodfclim1  12289  prodfap0  12290  efcvgfsum  12412  eftlub  12435  eflegeo  12446  tanval3ap  12459  tannegap  12473  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos01gt0  12508  bitsfzolem  12699  bitsfzo  12700  bitsinv1lem  12706  mulgcd  12771  nnminle  12790  eucalglt  12813  lcmledvds  12826  mulgcddvds  12850  prmind2  12876  isprm5lem  12897  pw2dvdslemn  12921  pw2dvdseulemle  12923  oddpwdclemdvds  12926  sqrt2irrap  12936  divdenle  12953  nonsq  12963  pythagtriplem4  13025  pclem0  13043  pcpremul  13050  pczdvds  13071  pcprmpw2  13090  qexpz  13109  4sqlem10  13144  ballotfilemimin  13227  ballotfilemsel1i  13234  ballotfilemro  13244  ennnfonelemkh  13281  triv1nsgd  13998  qusgrp  14012  gzsumsplit0  14125  prdsbaslemss  14151  bl2in  15427  xblcntrps  15437  xblcntr  15438  ssblps  15449  ssbl  15450  blssps  15451  blss  15452  xmetxp  15531  mulc1cncf  15613  cncfmptc  15620  mulcncflem  15631  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthdec  15668  ivthreinc  15669  hovera  15671  hoverlt1  15673  limcimolemlt  15688  cnplimclemle  15692  cnplimclemr  15693  limccnp2lem  15700  dveflem  15750  reeff1olem  15795  reeff1oleme  15796  tangtx  15862  cosq34lt1  15874  logdivlti  15905  cxpap0  15929  rpabscxpbnd  15965  pellexlem2  16006  mersenne  16025  lgslem3  16035  gausslemma2dlem1a  16091  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1c  16123  subumgredg2en  16426  qdencn  16977  cvgcmp2nlemabs  16986  trilpolemclim  16990  trilpolemisumle  16992  trilpolemeq1  16994  apdifflemf  17000  apdifflemr  17001