Theorem neneq 2964

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  necon3ad  2971  necon3ai  2983  2reu4lem  4484  elprn1  4617  elprn2  4618  pr1eqbg  4822  fpropnf1  7265  nf1const  7302  nelaneqOLDOLD  9562  gcd2n0cl  16562  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  ncoprmgcdne1b  16703  isnsgrp  18776  isnmnd  18791  mulmarep1gsum1  22730  fvmptnn04ifb  23008  tdeglem4  26217  isosctrlem2  26984  nnsge1  28536  structiedg0val  29372  umgr2edgneu  29564  imadifxp  32946  f1resrcmplf1dlem  35474  elttcirr  37062  aks6d1c2p2  42906  xppss12  43020  n0p  45785  supxrge  46074  uzn0bi  46193  liminflbuz2  46549  itgcoscmulx  46703  fourierdlem41  46882  elaa2  46968  sge0cl  47115  meadjiunlem  47199  hoidmvlelem2  47330  hspmbllem1  47360  chnerlem1  47618