Theorem neneqd 2330

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1332   ≠ wne 2309

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 2310

This theorem is referenced by:  neneq  2331  necon2bi  2364  necon2i  2365  pm2.21ddne  2392  nelrdva  2895  neq0r  3382  0inp0  4098  pwntru  4130  nndceq0  4539  frecabcl  6304  frecsuclem  6311  nnsucsssuc  6396  phpm  6767  diffisn  6795  en2eqpr  6809  fival  6866  omp1eomlem  6987  difinfsnlem  6992  difinfsn  6993  ctmlemr  7001  fodjuomnilemdc  7024  indpi  7174  nqnq0pi  7270  ltxrlt  7854  sup3exmid  8739  elnnz  9088  xrnemnf  9594  xrnepnf  9595  xrlttri3  9613  nltpnft  9627  ngtmnft  9630  xrpnfdc  9655  xrmnfdc  9656  xleaddadd  9700  fzprval  9893  fxnn0nninf  10242  iseqf1olemklt  10289  seq3f1olemqsumkj  10302  expnnval  10327  xrmaxrecl  11056  fsumcl2lem  11199  dvdsle  11578  mod2eq1n2dvds  11612  nndvdslegcd  11690  gcdnncl  11692  divgcdnn  11699  sqgcd  11753  eucalgf  11772  eucalginv  11773  lcmeq0  11788  lcmgcdlem  11794  qredeu  11814  rpdvds  11816  cncongr2  11821  divnumden  11910  divdenle  11911  phibndlem  11928  ennnfonelemk  11949  ennnfonelemjn  11951  ennnfonelemp1  11955  ennnfonelemim  11973  isxmet2d  12556  dvexp2  12884  logbgcd1irraplemexp  13093  nnsf  13374  peano4nninf  13375  exmidsbthrlem  13392  refeq  13398  trilpolemeq1  13408  dceqnconst  13423