Theorem difeq1i 3465

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

Syntax hints:   = wceq 1369   \ cdif 3320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-dif 3326

This theorem is referenced by:  difeq12i  3467  dfin3  3584  indif1  3589  indifcom  3590  difun1  3605  notab  3615  notrab  3622  undifabs  3751  difprsn1  4005  difprsn2  4006  orddif  4807  resdmdfsn  5147  fresaun  5577  domunsncan  7403  phplem1  7482  elfiun  7672  axcclem  8618  dfn2  10584  mvdco  15942  pmtrdifellem2  15974  islinds2  18217  lindsind2  18223  restcld  18751  bwthOLD  18989  ufprim  19457  volun  21001  itgsplitioo  21290  uhgra0v  23195  usgra0v  23241  usgra1v  23259  cusgra3v  23323  ex-dif  23581  imadifxp  25890  braew  26610  coinflippvt  26819  ballotlemfval0  26830  signstfvcl  26926  wfi  27619  frind  27655  onint1  28247  itg2addnclem  28396  asindmre  28432  kelac2  29371  f12dfv  30099  f13dfv  30100  lincext2  30878  bj-2upln1upl  32364