Theorem neneq 2936

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

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

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 207  df-ne 2931

This theorem is referenced by:  necon3ad  2943  necon3ai  2955  2reu4lem  4474  elprn1  4606  elprn2  4607  pr1eqbg  4811  fpropnf1  7211  nf1const  7248  nelaneqOLD  9505  gcd2n0cl  16434  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  ncoprmgcdne1b  16575  isnsgrp  18646  isnmnd  18661  mulmarep1gsum1  22515  fvmptnn04ifb  22793  tdeglem4  26019  isosctrlem2  26783  nnsge1  28303  structiedg0val  29044  umgr2edgneu  29236  imadifxp  32625  f1resrcmplf1dlem  35191  aks6d1c2p2  42312  xppss12  42427  n0p  45232  supxrge  45525  uzn0bi  45645  liminflbuz2  46001  itgcoscmulx  46155  fourierdlem41  46334  elaa2  46420  sge0cl  46567  meadjiunlem  46651  hoidmvlelem2  46782  hspmbllem1  46812  chnerlem1  47068