Theorem neneq 2962

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon3ad  2969  necon3ai  2981  2reu4lem  4479  elprn1  4612  elprn2  4613  pr1eqbg  4817  fpropnf1  7271  f1resrcmplf1dlem  7278  nf1const  7312  nelaneqOLDOLD  9598  gcd2n0cl  16679  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  ncoprmgcdne1b  16825  isnsgrp  18912  isnmnd  18927  mulmarep1gsum1  22888  fvmptnn04ifb  23169  tdeglem4  26378  isosctrlem2  27147  nnsge1  28729  structiedg0val  29600  umgr2edgneu  29795  imadifxp  33195  elttcirr  37319  aks6d1c2p2  43169  xppss12  43283  n0p  46061  supxrge  46349  uzn0bi  46468  liminflbuz2  46824  itgcoscmulx  46978  fourierdlem41  47157  elaa2  47243  sge0cl  47390  meadjiunlem  47474  hoidmvlelem2  47605  hspmbllem1  47635  chnerlem1  47891