Theorem neneq 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon3ad  2954  necon3ai  2966  2reu4lem  4521  pr1eqbg  4853  disjprgw  5139  fpropnf1  7253  nf1const  7289  nelaneq  9581  gcd2n0cl  16437  lcmfunsnlem2lem1  16562  lcmfunsnlem2lem2  16563  ncoprmgcdne1b  16574  isnsgrp  18601  isnmnd  18616  mulmarep1gsum1  22044  fvmptnn04ifb  22322  tdeglem4  25546  isosctrlem2  26291  structiedg0val  28249  umgr2edgneu  28438  imadifxp  31798  f1resrcmplf1dlem  34020  aks6d1c2p2  40863  xppss12  40963  n0p  43601  supxrge  43921  uzn0bi  44042  elprn1  44222  elprn2  44223  liminflbuz2  44404  itgcoscmulx  44558  fourierdlem41  44737  elaa2  44823  sge0cl  44970  meadjiunlem  45054  hoidmvlelem2  45185  hspmbllem1  45215