Theorem neneq 2939

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

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

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 2934

This theorem is referenced by:  necon3ad  2946  necon3ai  2958  2reu4lem  4478  elprn1  4610  elprn2  4611  pr1eqbg  4815  fpropnf1  7223  nf1const  7260  nelaneqOLD  9519  gcd2n0cl  16448  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  ncoprmgcdne1b  16589  isnsgrp  18660  isnmnd  18675  mulmarep1gsum1  22529  fvmptnn04ifb  22807  tdeglem4  26033  isosctrlem2  26797  nnsge1  28351  structiedg0val  29107  umgr2edgneu  29299  imadifxp  32688  f1resrcmplf1dlem  35263  aks6d1c2p2  42489  xppss12  42601  n0p  45405  supxrge  45697  uzn0bi  45817  liminflbuz2  46173  itgcoscmulx  46327  fourierdlem41  46506  elaa2  46592  sge0cl  46739  meadjiunlem  46823  hoidmvlelem2  46954  hspmbllem1  46984  chnerlem1  47240