Theorem eqbrtrd 3913

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

Syntax hints:   -> wi 4   = wceq 1312   class class class wbr 3893

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-br 3894

This theorem is referenced by:  eqbrtrrd  3915  dif1en  6724  prarloclemcalc  7252  ltexprlemopu  7353  recexprlemloc  7381  caucvgprprlemloccalc  7434  mulle0r  8606  lbinfle  8612  divge1  9403  xltnegi  9505  xleadd1a  9543  xltadd1  9546  xlt2add  9550  xposdif  9552  xleaddadd  9557  ubmelm1fzo  9890  qbtwnrelemcalc  9920  qbtwnxr  9922  ceiqm1l  9971  ceilqm1lt  9972  ceilqle  9974  modqlt  9993  modqeqmodmin  10054  addmodlteq  10058  exp3vallem  10181  bernneq  10299  faclbnd2  10375  resqrexlemdec  10669  resqrexlemcalc2  10673  resqrexlemglsq  10680  resqrexlemga  10681  abslt  10746  amgm2  10776  icodiamlt  10838  maxabsle  10862  maxltsup  10876  minmax  10887  min1inf  10889  min2inf  10890  bdtrilem  10896  xrmaxltsup  10913  xrmaxaddlem  10915  xrmaxadd  10916  xrminmax  10920  xrmin1inf  10922  xrmin2inf  10923  climconst  10945  serclim0  10960  mulcn2  10967  reccn2ap  10968  iserex  10994  climlec2  10996  iserge0  10998  climcau  11002  climcvg1nlem  11004  fsumabs  11120  iserabs  11130  isumlessdc  11151  divcnv  11152  expcnvre  11158  absgtap  11165  georeclim  11168  cvgratnnlembern  11178  cvgratnnlemsumlt  11183  cvgratnnlemfm  11184  cvgratnnlemrate  11185  mertenslemub  11189  mertenslemi1  11190  efcvgfsum  11218  eftlub  11241  eflegeo  11253  tanval3ap  11266  tannegap  11280  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  cos01gt0  11314  mulgcd  11544  eucalglt  11578  lcmledvds  11591  mulgcddvds  11615  prmind2  11641  pw2dvdslemn  11682  pw2dvdseulemle  11684  oddpwdclemdvds  11687  sqrt2irrap  11697  divdenle  11714  nonsq  11724  ennnfonelemkh  11764  bl2in  12386  xblcntrps  12396  xblcntr  12397  ssblps  12408  ssbl  12409  blssps  12410  blss  12411  xmetxp  12490  mulc1cncf  12556  cncfmptc  12562  mulcncflem  12570  limcimolemlt  12583  cnplimclemle  12587  cnplimclemr  12588  limccnp2lem  12595  qdencn  12903  cvgcmp2nlemabs  12908  trilpolemclim  12910  trilpolemisumle  12912  trilpolemeq1  12914