Theorem difeq1i 3603

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

Syntax hints:   = wceq 1383   \ cdif 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-dif 3464

This theorem is referenced by:  difeq12i  3605  dfin3  3722  indif1  3727  indifcom  3728  difun1  3743  notab  3753  notrab  3760  undifabs  3891  difprsn1  4151  difprsn2  4152  orddif  4961  resdmdfsn  5309  fresaun  5746  f12dfv  6164  f13dfv  6165  domunsncan  7619  phplem1  7698  elfiun  7892  axcclem  8840  dfn2  10815  mvdco  16449  pmtrdifellem2  16481  islinds2  18826  lindsind2  18832  restcld  19651  bwthOLD  19889  ufprim  20388  volun  21933  itgsplitioo  22222  uhgra0v  24288  usgra0v  24349  usgra1v  24368  cusgra3v  24442  ex-dif  25122  imadifxp  27436  braew  28192  coinflippvt  28401  ballotlemfval0  28412  signstfvcl  28508  wfi  29263  frind  29299  onint1  29890  itg2addnclem  30042  asindmre  30078  kelac2  30987  fourierdlem102  31945  fourierdlem114  31957  uhg0v  32331  uhgrepe  32332  lincext2  32926  bj-2upln1upl  34465