Theorem neneq 2788

Description: From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
neneq	⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneq

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
2	1	neneqd 2787	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-ne 2782

This theorem is referenced by:  necon3ad  2795  nelsnOLD  4160  hash2prd  13114  fprodn0f  14561  gcd2n0cl  15069  lcmfunsnlem2lem1  15189  structiedg0val  25699  n0p  38234  supxrge  38495  elprn1  38700  elprn2  38701  itgcoscmulx  38861  fourierdlem41  39041  elaa2  39127  sge0cl  39274  meadjiunlem  39358  hoidmvlelem2  39486  hspmbllem1  39516  fpropnf1  40337  umgr2edgneu  40441  clwwlknclwwlkdifs  41181  av-numclwwlk3lem  41538