Theorem difeq1i 3618

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 3615	. 2 |- ( A = B -> ( A \ C ) = ( B \ C ) )
3	1, 2	ax-mp 5	1 |- ( A \ C ) = ( B \ C )

Syntax hints:   = wceq 1379   \ cdif 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-dif 3479

This theorem is referenced by:  difeq12i  3620  dfin3  3737  indif1  3742  indifcom  3743  difun1  3758  notab  3768  notrab  3775  undifabs  3904  difprsn1  4163  difprsn2  4164  orddif  4971  resdmdfsn  5317  fresaun  5754  f12dfv  6165  f13dfv  6166  domunsncan  7614  phplem1  7693  elfiun  7886  axcclem  8833  dfn2  10804  mvdco  16266  pmtrdifellem2  16298  islinds2  18615  lindsind2  18621  restcld  19439  bwthOLD  19677  ufprim  20145  volun  21690  itgsplitioo  21979  uhgra0v  23986  usgra0v  24047  usgra1v  24066  cusgra3v  24140  ex-dif  24821  imadifxp  27131  braew  27854  coinflippvt  28063  ballotlemfval0  28074  signstfvcl  28170  wfi  28864  frind  28900  onint1  29491  itg2addnclem  29643  asindmre  29679  kelac2  30615  fourierdlem102  31509  fourierdlem114  31521  uhg0v  31846  uhgrepe  31847  lincext2  32129  bj-2upln1upl  33663