Theorem difeq1i 3576

Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	|- A = B

Assertion

Ref	Expression
difeq1i	|- ( A \ C ) = ( B \ C )

Proof of Theorem difeq1i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 |- A = B
2		difeq1 3573	. 2 |- ( A = B -> ( A \ C ) = ( B \ C ) )
3	1, 2	ax-mp 5	1 |- ( A \ C ) = ( B \ C )

Syntax hints:   = wceq 1437   \ cdif 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-dif 3436

This theorem is referenced by:  difeq12i  3578  dfin3  3709  indif1  3714  indifcom  3715  difun1  3730  notab  3740  notrab  3747  undifabs  3869  difprsn1  4130  difprsn2  4131  resdmdfsn  5161  wfi  5423  orddif  5526  fresaun  5762  f12dfv  6178  f13dfv  6179  domunsncan  7669  phplem1  7748  elfiun  7941  axcclem  8876  dfn2  10871  mvdco  17030  pmtrdifellem2  17062  islinds2  19295  lindsind2  19301  restcld  20112  ufprim  20848  volun  22372  itgsplitioo  22669  uhgra0v  24880  usgra0v  24941  usgra1v  24960  cusgra3v  25034  ex-dif  25715  indifundif  27985  imadifxp  28048  aciunf1  28102  braew  28901  carsgclctunlem1  28975  carsggect  28976  coinflippvt  29140  ballotlemfval0  29151  signstfvcl  29247  frind  30265  onint1  30891  bj-2upln1upl  31364  poimirlem13  31657  poimirlem14  31658  poimirlem18  31662  poimirlem21  31665  poimirlem30  31674  itg2addnclem  31697  asindmre  31731  kelac2  35633  fourierdlem102  37644  fourierdlem114  37656  pwsal  37727  sge0fodjrnlem  37796  uhg0v  38460  uhgrepe  38461  lincext2  39021