Theorem neneqd 2329

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1331   ≠ wne 2308

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 2309

This theorem is referenced by:  neneq  2330  necon2bi  2363  necon2i  2364  pm2.21ddne  2391  nelrdva  2891  neq0r  3377  0inp0  4090  pwntru  4122  nndceq0  4531  frecabcl  6296  frecsuclem  6303  nnsucsssuc  6388  phpm  6759  diffisn  6787  en2eqpr  6801  fival  6858  omp1eomlem  6979  difinfsnlem  6984  difinfsn  6985  ctmlemr  6993  fodjuomnilemdc  7016  indpi  7150  nqnq0pi  7246  ltxrlt  7830  sup3exmid  8715  elnnz  9064  xrnemnf  9564  xrnepnf  9565  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  xrpnfdc  9625  xrmnfdc  9626  xleaddadd  9670  fzprval  9862  fxnn0nninf  10211  iseqf1olemklt  10258  seq3f1olemqsumkj  10271  expnnval  10296  xrmaxrecl  11024  fsumcl2lem  11167  dvdsle  11542  mod2eq1n2dvds  11576  nndvdslegcd  11654  gcdnncl  11656  divgcdnn  11663  sqgcd  11717  eucalgf  11736  eucalginv  11737  lcmeq0  11752  lcmgcdlem  11758  qredeu  11778  rpdvds  11780  cncongr2  11785  divnumden  11874  divdenle  11875  phibndlem  11892  ennnfonelemk  11913  ennnfonelemjn  11915  ennnfonelemp1  11919  ennnfonelemim  11937  isxmet2d  12517  dvexp2  12845  nnsf  13199  peano4nninf  13200  exmidsbthrlem  13217  refeq  13223  trilpolemeq1  13233