Theorem eqbrtrd 3945

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

Syntax hints:   -> wi 4   = wceq 1331   class class class wbr 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925

This theorem is referenced by:  eqbrtrrd  3947  dif1en  6766  ccfunen  7072  prarloclemcalc  7303  ltexprlemopu  7404  recexprlemloc  7432  caucvgprprlemloccalc  7485  suplocsrlem  7609  axpre-suploclemres  7702  mulle0r  8695  lbinfle  8701  divge1  9503  xltnegi  9611  xleadd1a  9649  xltadd1  9652  xlt2add  9656  xposdif  9658  xleaddadd  9663  ubmelm1fzo  9996  qbtwnrelemcalc  10026  qbtwnxr  10028  ceiqm1l  10077  ceilqm1lt  10078  ceilqle  10080  modqlt  10099  modqeqmodmin  10160  addmodlteq  10164  exp3vallem  10287  bernneq  10405  faclbnd2  10481  resqrexlemdec  10776  resqrexlemcalc2  10780  resqrexlemglsq  10787  resqrexlemga  10788  abslt  10853  amgm2  10883  icodiamlt  10945  maxabsle  10969  maxltsup  10983  minmax  10994  min1inf  10996  min2inf  10997  bdtrilem  11003  xrmaxltsup  11020  xrmaxaddlem  11022  xrmaxadd  11023  xrminmax  11027  xrmin1inf  11029  xrmin2inf  11030  climconst  11052  serclim0  11067  mulcn2  11074  reccn2ap  11075  iserex  11101  climlec2  11103  iserge0  11105  climcau  11109  climcvg1nlem  11111  fsumabs  11227  iserabs  11237  isumlessdc  11258  divcnv  11259  expcnvre  11265  absgtap  11272  georeclim  11275  cvgratnnlembern  11285  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratnnlemrate  11292  mertenslemub  11296  mertenslemi1  11297  prodfclim1  11306  prodfap0  11307  efcvgfsum  11362  eftlub  11385  eflegeo  11397  tanval3ap  11410  tannegap  11424  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  cos01gt0  11458  mulgcd  11693  eucalglt  11727  lcmledvds  11740  mulgcddvds  11764  prmind2  11790  pw2dvdslemn  11832  pw2dvdseulemle  11834  oddpwdclemdvds  11837  sqrt2irrap  11847  divdenle  11864  nonsq  11874  ennnfonelemkh  11914  bl2in  12561  xblcntrps  12571  xblcntr  12572  ssblps  12583  ssbl  12584  blssps  12585  blss  12586  xmetxp  12665  mulc1cncf  12734  cncfmptc  12740  mulcncflem  12748  ivthinclemlopn  12772  ivthinclemuopn  12774  ivthdec  12780  limcimolemlt  12791  cnplimclemle  12795  cnplimclemr  12796  limccnp2lem  12803  dveflem  12844  tangtx  12908  cosq34lt1  12920  qdencn  13211  cvgcmp2nlemabs  13216  trilpolemclim  13218  trilpolemisumle  13220  trilpolemeq1  13222