Theorem eqbrtrd 3805

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

Syntax hints:   -> wi 4   = wceq 1284   class class class wbr 3785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  eqbrtrrd  3807  dif1en  6364  prarloclemcalc  6692  ltexprlemopu  6793  recexprlemloc  6821  caucvgprprlemloccalc  6874  mulle0r  8022  lbinfle  8028  divge1  8800  xltnegi  8902  ubmelm1fzo  9235  qbtwnrelemcalc  9264  qbtwnxr  9266  ceiqm1l  9313  ceilqm1lt  9314  ceilqle  9316  modqlt  9335  modqeqmodmin  9396  addmodlteq  9400  bernneq  9593  faclbnd2  9669  resqrexlemdec  9897  resqrexlemcalc2  9901  resqrexlemglsq  9908  resqrexlemga  9909  abslt  9974  amgm2  10004  icodiamlt  10066  maxabsle  10090  maxltsup  10104  minmax  10112  min1inf  10113  min2inf  10114  climconst  10129  iserclim0  10144  mulcn2  10151  iiserex  10177  climlec2  10179  iserige0  10181  climcau  10184  climcvg1nlem  10186  mulgcd  10405  eucalglt  10439  lcmledvds  10452  mulgcddvds  10476  prmind2  10502  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdclemdvds  10548  sqrt2irrap  10558  qdencn  10785