Theorem neneq 2938

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

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

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 2933

This theorem is referenced by:  necon3ad  2945  necon3ai  2957  2reu4lem  4476  elprn1  4608  elprn2  4609  pr1eqbg  4813  fpropnf1  7213  nf1const  7250  nelaneqOLD  9507  gcd2n0cl  16436  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  ncoprmgcdne1b  16577  isnsgrp  18648  isnmnd  18663  mulmarep1gsum1  22517  fvmptnn04ifb  22795  tdeglem4  26021  isosctrlem2  26785  nnsge1  28339  structiedg0val  29095  umgr2edgneu  29287  imadifxp  32676  f1resrcmplf1dlem  35242  aks6d1c2p2  42383  xppss12  42495  n0p  45300  supxrge  45593  uzn0bi  45713  liminflbuz2  46069  itgcoscmulx  46223  fourierdlem41  46402  elaa2  46488  sge0cl  46635  meadjiunlem  46719  hoidmvlelem2  46850  hspmbllem1  46880  chnerlem1  47136