Theorem neneq 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  necon3ad  2956  necon3ai  2968  2reu4lem  4456  pr1eqbg  4787  disjprgw  5069  fpropnf1  7140  nf1const  7176  nelaneq  9358  gcd2n0cl  16216  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  ncoprmgcdne1b  16355  isnsgrp  18379  isnmnd  18389  mulmarep1gsum1  21722  fvmptnn04ifb  22000  tdeglem4  25224  isosctrlem2  25969  structiedg0val  27392  umgr2edgneu  27581  imadifxp  30940  f1resrcmplf1dlem  33058  xppss12  40204  n0p  42591  supxrge  42877  uzn0bi  42999  elprn1  43174  elprn2  43175  liminflbuz2  43356  itgcoscmulx  43510  fourierdlem41  43689  elaa2  43775  sge0cl  43919  meadjiunlem  44003  hoidmvlelem2  44134  hspmbllem1  44164