Theorem difeq1i 3547

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

Syntax hints:   = wceq 1444   \ cdif 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-dif 3407

This theorem is referenced by:  difeq12i  3549  dfin3  3682  indif1  3687  indifcom  3688  difun1  3703  notab  3713  notrab  3720  undifabs  3844  difprsn1  4108  difprsn2  4109  resdmdfsn  5150  wfi  5413  orddif  5516  fresaun  5754  f12dfv  6172  f13dfv  6173  domunsncan  7672  phplem1  7751  elfiun  7944  axcclem  8887  dfn2  10882  mvdco  17086  pmtrdifellem2  17118  islinds2  19371  lindsind2  19377  restcld  20188  ufprim  20924  volun  22498  itgsplitioo  22795  uhgra0v  25037  usgra0v  25098  usgra1v  25117  cusgra3v  25192  ex-dif  25873  indifundif  28152  imadifxp  28212  aciunf1  28265  braew  29065  carsgclctunlem1  29149  carsggect  29150  coinflippvt  29317  ballotlemfval0  29328  signstfvcl  29462  frind  30481  onint1  31109  bj-2upln1upl  31618  poimirlem13  31953  poimirlem14  31954  poimirlem18  31958  poimirlem21  31961  poimirlem30  31970  itg2addnclem  31993  asindmre  32027  kelac2  35923  fourierdlem102  38072  fourierdlem114  38084  pwsal  38176  issald  38192  sge0fodjrnlem  38258  hoiprodp1  38410  uhgr0vb  39165  uhgr0  39166  usgr1vr  39329  uvtxupgrres  39481  cplgr3v  39502  uhg0v  39742  uhgrepe  39743  lincext2  40301