Theorem neneq 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  necon3ad  2947  necon3ai  2959  2reu4lem  4451  elprn1  4583  elprn2  4584  pr1eqbg  4788  fpropnf1  7211  nf1const  7248  nelaneqOLDOLD  9509  gcd2n0cl  16469  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  ncoprmgcdne1b  16610  isnsgrp  18682  isnmnd  18697  mulmarep1gsum1  22556  fvmptnn04ifb  22834  tdeglem4  26043  isosctrlem2  26801  nnsge1  28353  structiedg0val  29109  umgr2edgneu  29301  imadifxp  32690  f1resrcmplf1dlem  35267  elttcirr  36759  aks6d1c2p2  42604  xppss12  42716  n0p  45493  supxrge  45783  uzn0bi  45902  liminflbuz2  46258  itgcoscmulx  46412  fourierdlem41  46591  elaa2  46677  sge0cl  46824  meadjiunlem  46908  hoidmvlelem2  47039  hspmbllem1  47069  chnerlem1  47327