Theorem neneq 2970

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 23	. 2 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
2	1	neneqd 2969	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  necon3ad  2977  necon3ai  2989  2reu4lem  4489  elprn1  4622  elprn2  4623  pr1eqbg  4826  fpropnf1  7266  nf1const  7303  nelaneqOLDOLD  9566  gcd2n0cl  16567  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  ncoprmgcdne1b  16708  isnsgrp  18781  isnmnd  18796  mulmarep1gsum1  22699  fvmptnn04ifb  22977  tdeglem4  26186  isosctrlem2  26950  nnsge1  28502  structiedg0val  29313  umgr2edgneu  29505  imadifxp  32887  f1resrcmplf1dlem  35418  elttcirr  36931  aks6d1c2p2  42776  xppss12  42890  n0p  45657  supxrge  45946  uzn0bi  46065  liminflbuz2  46421  itgcoscmulx  46575  fourierdlem41  46754  elaa2  46840  sge0cl  46987  meadjiunlem  47071  hoidmvlelem2  47202  hspmbllem1  47232  chnerlem1  47490