Theorem difeq1d 3727

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

Hypothesis

Ref	Expression
difeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
difeq1d	|- ( ph -> ( A \ C ) = ( B \ C ) )

Proof of Theorem difeq1d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 |- ( ph -> A = B )
2		difeq1 3721	. 2 |- ( A = B -> ( A \ C ) = ( B \ C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A \ C ) = ( B \ C ) )

Syntax hints:   -> wi 4   = wceq 1483   \ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-dif 3577

This theorem is referenced by:  difeq12d  3729  diftpsn3OLD  4333  dffv2  6271  phplem4  8142  unfilem3  8226  marypha1lem  8339  infdifsn  8554  cantnfp1lem3  8577  en2other2  8832  isacn  8867  cda1dif  8998  fin23lem28  9162  enfin1ai  9206  fin1a2lem7  9228  fzdifsuc  12400  axdc4uz  12783  leiso  13243  cshimadifsn  13575  isstruct2  15867  setsfun0  15894  strle1  15973  pltfval  16959  f1omvdco2  17868  symgsssg  17887  symgfisg  17888  symggen  17890  pmtrdifellem3  17898  pmtrdifwrdellem3  17903  pmtrdifwrdel2lem1  17904  pmtrdifwrdel  17905  pmtrdifwrdel2  17906  psgnunilem1  17913  psgnunilem5  17914  psgnunilem2  17915  psgnunilem3  17916  gsumval3  18308  dmdprd  18397  dprd2da  18441  dmdprdsplit2lem  18444  dpjfval  18454  ablfac1eulem  18471  lssset  18934  lbspropd  19099  opsrtoslem2  19485  islindf  20151  islindf2  20153  f1lindf  20161  cldval  20827  difopn  20838  mretopd  20896  restcld  20976  ordtcld1  21001  ordtcld2  21002  cnclima  21072  iscncl  21073  isreg2  21181  llycmpkgen2  21353  1stckgen  21357  ptval  21373  txcld  21406  ptcld  21416  txkgen  21455  qtopcld  21516  qtoprest  21520  qtopcmap  21522  kqcldsat  21536  regr1lem  21542  trufil  21714  ufildr  21735  opnsubg  21911  cldsubg  21914  blcld  22310  lebnumlem1  22760  bcthlem1  23121  bcth  23126  bcth3  23128  difmbl  23311  itg1val  23450  itgioo  23582  limciun  23658  dvfval  23661  istrkgl  25357  ishpg  25651  eengv  25859  elntg  25864  isuhgr  25955  isushgr  25956  uhgreq12g  25960  isuhgrop  25965  uhgr0vb  25967  uhgrun  25969  uhgrstrrepe  25973  isupgr  25979  upgrop  25989  isumgr  25990  upgrun  26013  isuspgr  26047  isusgr  26048  isuspgrop  26056  nb3grprlem2  26283  uvtxaval  26287  nbupgruvtxres  26308  cplgrop  26333  cusgrexi  26339  structtocusgr  26342  1loopgrnb0  26398  isconngr1  27050  isfrgr  27122  frgr3v  27139  difuncomp  29369  imadifxp  29414  gtiso  29478  difico  29545  fzdif2  29551  fzodif2  29552  submarchi  29740  qtophaus  29903  imambfm  30324  difelcarsg  30372  carsgclctunlem1  30379  carsggect  30380  issibf  30395  sibf0  30396  sitgfval  30403  ballotlemfval  30551  ballotlemfp1  30553  ballotlemgun  30586  hgt750lemb  30734  kur14  31198  iscvm  31241  cvmscld  31255  mdvval  31401  topbnd  32319  poimirlem2  33411  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem18  33427  poimirlem19  33428  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem27  33436  poimirlem30  33439  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnclem2  33462  aomclem8  37631  kelac2  37635  gneispace2  38430  fzdifsuc2  39525  iccdifioo  39741  iccdifprioo  39742  ibliooicc  40187  dirkercncflem2  40321  issal  40534  prsal  40538  saldifcl2  40546  intsal  40548  sge0fodjrnlem  40633  caratheodorylem1  40740  vonvolmbllem  40874  salpreimagelt  40918  salpreimalegt  40920  smfresal  40995