Theorem neneqd 2433

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 2413	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 122	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-ne 2413

This theorem is referenced by:  neneq  2434  necon2bi  2467  necon2i  2468  pm2.21ddne  2495  nelrdva  3024  neq0r  3523  ifnetruedc  3666  ifnefals  3667  0inp0  4279  pwntru  4312  nndceq0  4740  fczsupp0  6459  frecabcl  6630  frecsuclem  6637  nnsucsssuc  6725  phpm  7120  diffisn  7150  en2eqpr  7167  fival  7257  omp1eomlem  7385  difinfsnlem  7390  difinfsn  7391  ctmlemr  7399  nninfisollemne  7422  fodjuomnilemdc  7435  exmidapne  7574  indpi  7657  nqnq0pi  7753  ltxrlt  8339  sup3exmid  9231  elnnz  9587  xrnemnf  10110  xrnepnf  10111  xrlttri3  10130  nltpnft  10147  ngtmnft  10150  xrpnfdc  10175  xrmnfdc  10176  xleaddadd  10220  fzprval  10416  fzodisjsn  10518  xqltnle  10627  fxnn0nninf  10801  iseqf1olemklt  10860  seq3f1olemqsumkj  10873  expnnval  10904  fihashelne0d  11160  xrmaxrecl  11940  fsumcl2lem  12084  fprodcl2lem  12291  dvdsle  12530  mod2eq1n2dvds  12565  nndvdslegcd  12661  gcdnncl  12663  divgcdnn  12671  sqgcd  12725  eucalgf  12752  eucalginv  12753  lcmeq0  12768  lcmgcdlem  12774  qredeu  12794  rpdvds  12796  cncongr2  12801  divnumden  12893  divdenle  12894  phibndlem  12913  phisum  12938  oddprm  12957  pythagtriplem4  12966  pythagtriplem8  12970  pythagtriplem9  12971  pceq0  13020  4sqlem10  13085  ennnfonelemk  13151  ennnfonelemjn  13153  ennnfonelemp1  13157  ennnfonelemim  13175  mulgnn  13843  rrgnz  14414  aprirr  14429  isxmet2d  15213  dvexp2  15577  dvply1  15630  logbgcd1irraplemexp  15833  perfectlem2  15868  lgsval2lem  15883  lgsval4  15893  lgsdilem  15900  lgsdir  15908  gausslemma2dlem4  15937  lgseisenlem4  15946  lgsquadlem1  15950  lgsquad2  15956  m1lgs  15958  2sqlem8a  15995  2sqlem8  15996  uhgr2edg  16201  usgr1vr  16243  vdegp1aid  16309  g0wlk0  16365  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  depindlem1  16501  pw1ndom3lem  16763  nnsf  16783  peano4nninf  16784  exmidsbthrlem  16802  refeq  16808  trilpolemeq1  16824  qdiff  16833  dceqnconst  16846