Theorem neneqd 2266

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1284   ≠ wne 2245

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

This theorem depends on definitions:  df-bi 115  df-ne 2246

This theorem is referenced by:  neneq  2267  necon2bi  2300  necon2i  2301  pm2.21ddne  2328  nelrdva  2797  neq0r  3262  0inp0  3940  nndceq0  4357  frecsuclem3  6013  nnsucsssuc  6094  phpm  6351  diffisn  6377  en2eqpr  6380  indpi  6532  nqnq0pi  6628  ltxrlt  7178  elnnz  8361  xrnemnf  8853  xrnepnf  8854  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  fzprval  9099  expival  9478  expinnval  9479  dvdsle  10244  mod2eq1n2dvds  10279  nndvdslegcd  10357  gcdnncl  10359  divgcdnn  10366  sqgcd  10418  eucalgf  10437  eucalginv  10438  lcmeq0  10453  lcmgcdlem  10459  qredeu  10479  rpdvds  10481  cncongr2  10486