Theorem neneq 2934

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

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

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 2929

This theorem is referenced by:  necon3ad  2941  necon3ai  2953  2reu4lem  4469  elprn1  4601  elprn2  4602  pr1eqbg  4806  fpropnf1  7201  nf1const  7238  nelaneqOLD  9488  gcd2n0cl  16420  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  ncoprmgcdne1b  16561  isnsgrp  18631  isnmnd  18646  mulmarep1gsum1  22488  fvmptnn04ifb  22766  tdeglem4  25992  isosctrlem2  26756  nnsge1  28271  structiedg0val  29000  umgr2edgneu  29192  imadifxp  32581  f1resrcmplf1dlem  35098  aks6d1c2p2  42222  xppss12  42332  n0p  45152  supxrge  45447  uzn0bi  45567  liminflbuz2  45923  itgcoscmulx  46077  fourierdlem41  46256  elaa2  46342  sge0cl  46489  meadjiunlem  46573  hoidmvlelem2  46704  hspmbllem1  46734  chnerlem1  46990