Theorem neneq 2945

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 2944	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2939

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 206  df-ne 2940

This theorem is referenced by:  necon3ad  2952  necon3ai  2964  2reu4lem  4488  pr1eqbg  4819  disjprgw  5105  fpropnf1  7219  nf1const  7255  nelaneq  9544  gcd2n0cl  16400  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  ncoprmgcdne1b  16537  isnsgrp  18564  isnmnd  18574  mulmarep1gsum1  21959  fvmptnn04ifb  22237  tdeglem4  25461  isosctrlem2  26206  structiedg0val  28036  umgr2edgneu  28225  imadifxp  31586  f1resrcmplf1dlem  33779  aks6d1c2p2  40622  xppss12  40723  n0p  43373  supxrge  43693  uzn0bi  43814  elprn1  43994  elprn2  43995  liminflbuz2  44176  itgcoscmulx  44330  fourierdlem41  44509  elaa2  44595  sge0cl  44742  meadjiunlem  44826  hoidmvlelem2  44957  hspmbllem1  44987