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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon3ad  2969  necon3ai  2981  2reu4lem  4476  elprn1  4609  elprn2  4610  pr1eqbg  4814  fpropnf1  7245  nf1const  7282  nelaneqOLDOLD  9547  gcd2n0cl  16524  lcmfunsnlem2lem1  16653  lcmfunsnlem2lem2  16654  ncoprmgcdne1b  16665  isnsgrp  18738  isnmnd  18753  mulmarep1gsum1  22611  fvmptnn04ifb  22889  tdeglem4  26098  isosctrlem2  26859  nnsge1  28411  structiedg0val  29167  umgr2edgneu  29359  imadifxp  32748  f1resrcmplf1dlem  35342  elttcirr  36844  aks6d1c2p2  42689  xppss12  42801  n0p  45578  supxrge  45867  uzn0bi  45986  liminflbuz2  46342  itgcoscmulx  46496  fourierdlem41  46675  elaa2  46761  sge0cl  46908  meadjiunlem  46992  hoidmvlelem2  47123  hspmbllem1  47153  chnerlem1  47411