Theorem neneqd 2441

Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
neneqd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
neneqd	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneqd

Step	Hyp	Ref	Expression
1		neneqd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		df-ne 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 122	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neneq  2442  necon2bi  2475  necon2i  2476  pm2.21ddne  2503  nelrdva  3033  neq0r  3536  ifnetruedc  3684  ifnefals  3685  0inp0  4305  pwntru  4338  nndceq0  4767  fczsupp0  6503  frecabcl  6674  frecsuclem  6681  nnsucsssuc  6769  phpm  7171  diffisn  7201  en2eqpr  7218  fival  7309  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctmlemr  7454  nninfisollemne  7477  fodjuomnilemdc  7490  exmidapne  7632  indpi  7715  nqnq0pi  7811  ltxrlt  8397  sup3exmid  9295  elnnz  9665  xrnemnf  10196  xrnepnf  10197  xrlttri3  10216  nltpnft  10233  ngtmnft  10236  xrpnfdc  10261  xrmnfdc  10262  xleaddadd  10306  fzprval  10506  fzodisjsn  10608  xqltnle  10719  fxnn0nninf  10897  iseqf1olemklt  10956  seq3f1olemqsumkj  10969  expnnval  11000  fihashelne0d  11258  xrmaxrecl  12046  fsumcl2lem  12190  fprodcl2lem  12397  dvdsle  12636  mod2eq1n2dvds  12671  nndvdslegcd  12767  gcdnncl  12769  divgcdnn  12777  sqgcd  12831  eucalgf  12858  eucalginv  12859  lcmeq0  12874  lcmgcdlem  12880  qredeu  12900  rpdvds  12902  cncongr2  12907  divnumden  13001  divdenle  13002  phibndlem  13023  phisum  13048  oddprm  13067  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  pceq0  13130  4sqlem10  13195  ballotfilemirc  13333  ennnfonelemk  13349  ennnfonelemjn  13351  ennnfonelemp1  13355  ennnfonelemim  13373  mulgnn  13988  rrgnz  14686  aprirr  14704  isxmet2d  15574  dvexp2  15938  dvply1  15991  logbgcd1irraplemexp  16204  perfectlem2  16300  lgsval2lem  16334  lgsval4  16344  lgsdilem  16351  lgsdir  16359  gausslemma2dlem4  16388  lgseisenlem4  16397  lgsquadlem1  16401  lgsquad2  16407  m1lgs  16409  2sqlem8a  16446  2sqlem8  16447  uhgr2edg  16652  usgr1vr  16694  vdegp1aid  16760  g0wlk0  16816  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  depindlem1  16952  dichmul0orlem5  16962  dichmul0orlem6  16963  pw1ndom3lem  17224  nnsf  17254  peano4nninf  17255  exmidsbthrlem  17273  refeq  17279  trilpolemeq1  17296  qdiff  17305  dceqnconst  17317