Theorem neneqd 2361

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1348   ≠ wne 2340

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 2341

This theorem is referenced by:  neneq  2362  necon2bi  2395  necon2i  2396  pm2.21ddne  2423  nelrdva  2937  neq0r  3429  0inp0  4152  pwntru  4185  nndceq0  4602  frecabcl  6378  frecsuclem  6385  nnsucsssuc  6471  phpm  6843  diffisn  6871  en2eqpr  6885  fival  6947  omp1eomlem  7071  difinfsnlem  7076  difinfsn  7077  ctmlemr  7085  nninfisollemne  7107  fodjuomnilemdc  7120  indpi  7304  nqnq0pi  7400  ltxrlt  7985  sup3exmid  8873  elnnz  9222  xrnemnf  9734  xrnepnf  9735  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrpnfdc  9799  xrmnfdc  9800  xleaddadd  9844  fzprval  10038  fxnn0nninf  10394  iseqf1olemklt  10441  seq3f1olemqsumkj  10454  expnnval  10479  fihashelne0d  10732  xrmaxrecl  11218  fsumcl2lem  11361  fprodcl2lem  11568  dvdsle  11804  mod2eq1n2dvds  11838  nndvdslegcd  11920  gcdnncl  11922  divgcdnn  11930  sqgcd  11984  eucalgf  12009  eucalginv  12010  lcmeq0  12025  lcmgcdlem  12031  qredeu  12051  rpdvds  12053  cncongr2  12058  divnumden  12150  divdenle  12151  phibndlem  12170  phisum  12194  oddprm  12213  pythagtriplem4  12222  pythagtriplem8  12226  pythagtriplem9  12227  pceq0  12275  4sqlem10  12339  ennnfonelemk  12355  ennnfonelemjn  12357  ennnfonelemp1  12361  ennnfonelemim  12379  isxmet2d  13142  dvexp2  13470  logbgcd1irraplemexp  13680  lgsval2lem  13705  lgsval4  13715  lgsdilem  13722  lgsdir  13730  2sqlem8a  13752  2sqlem8  13753  nnsf  14038  peano4nninf  14039  exmidsbthrlem  14054  refeq  14060  trilpolemeq1  14072  dceqnconst  14091