Theorem neneqd 2226

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1243   ≠ wne 2204

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

This theorem depends on definitions:  df-bi 110  df-ne 2206

This theorem is referenced by:  neneq  2227  necon2bi  2260  necon2i  2261  pm2.21ddne  2288  nelrdva  2746  neq0r  3235  0inp0  3919  nndceq0  4339  frecsuclem3  5990  nnsucsssuc  6071  phpm  6327  diffisn  6350  indpi  6440  nqnq0pi  6536  ltxrlt  7085  elnnz  8255  xrnemnf  8699  xrnepnf  8700  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  fzprval  8944  expival  9257  expinnval  9258