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  7153  nqnq0pi  7249  ltxrlt  7833  sup3exmid  8718  elnnz  9067  xrnemnf  9567  xrnepnf  9568  xrlttri3  9586  nltpnft  9600  ngtmnft  9603  xrpnfdc  9628  xrmnfdc  9629  xleaddadd  9673  fzprval  9865  fxnn0nninf  10214  iseqf1olemklt  10261  seq3f1olemqsumkj  10274  expnnval  10299  xrmaxrecl  11027  fsumcl2lem  11170  dvdsle  11545  mod2eq1n2dvds  11579  nndvdslegcd  11657  gcdnncl  11659  divgcdnn  11666  sqgcd  11720  eucalgf  11739  eucalginv  11740  lcmeq0  11755  lcmgcdlem  11761  qredeu  11781  rpdvds  11783  cncongr2  11788  divnumden  11877  divdenle  11878  phibndlem  11895  ennnfonelemk  11916  ennnfonelemjn  11918  ennnfonelemp1  11922  ennnfonelemim  11940  isxmet2d  12520  dvexp2  12848  nnsf  13202  peano4nninf  13203  exmidsbthrlem  13220  refeq  13226  trilpolemeq1  13236