Theorem neneqd 2356

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1343   ≠ wne 2335

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

This theorem depends on definitions:  df-bi 116  df-ne 2336

This theorem is referenced by:  neneq  2357  necon2bi  2390  necon2i  2391  pm2.21ddne  2418  nelrdva  2932  neq0r  3422  0inp0  4144  pwntru  4177  nndceq0  4594  frecabcl  6363  frecsuclem  6370  nnsucsssuc  6456  phpm  6827  diffisn  6855  en2eqpr  6869  fival  6931  omp1eomlem  7055  difinfsnlem  7060  difinfsn  7061  ctmlemr  7069  nninfisollemne  7091  fodjuomnilemdc  7104  indpi  7279  nqnq0pi  7375  ltxrlt  7960  sup3exmid  8848  elnnz  9197  xrnemnf  9709  xrnepnf  9710  xrlttri3  9729  nltpnft  9746  ngtmnft  9749  xrpnfdc  9774  xrmnfdc  9775  xleaddadd  9819  fzprval  10013  fxnn0nninf  10369  iseqf1olemklt  10416  seq3f1olemqsumkj  10429  expnnval  10454  xrmaxrecl  11192  fsumcl2lem  11335  fprodcl2lem  11542  dvdsle  11778  mod2eq1n2dvds  11812  nndvdslegcd  11894  gcdnncl  11896  divgcdnn  11904  sqgcd  11958  eucalgf  11983  eucalginv  11984  lcmeq0  11999  lcmgcdlem  12005  qredeu  12025  rpdvds  12027  cncongr2  12032  divnumden  12124  divdenle  12125  phibndlem  12144  phisum  12168  oddprm  12187  pythagtriplem4  12196  pythagtriplem8  12200  pythagtriplem9  12201  pceq0  12249  4sqlem10  12313  ennnfonelemk  12329  ennnfonelemjn  12331  ennnfonelemp1  12335  ennnfonelemim  12353  isxmet2d  12948  dvexp2  13276  logbgcd1irraplemexp  13486  lgsval2lem  13511  lgsval4  13521  lgsdilem  13528  lgsdir  13536  2sqlem8a  13558  2sqlem8  13559  nnsf  13845  peano4nninf  13846  exmidsbthrlem  13861  refeq  13867  trilpolemeq1  13879  dceqnconst  13898