Theorem neneq 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon3ad  2951  necon3ai  2963  2reu4lem  4528  pr1eqbg  4862  fpropnf1  7287  nf1const  7324  nelaneq  9637  gcd2n0cl  16543  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  ncoprmgcdne1b  16684  isnsgrp  18749  isnmnd  18764  mulmarep1gsum1  22595  fvmptnn04ifb  22873  tdeglem4  26114  isosctrlem2  26877  nnsge1  28361  structiedg0val  29054  umgr2edgneu  29246  imadifxp  32621  f1resrcmplf1dlem  35079  aks6d1c2p2  42101  xppss12  42247  n0p  44983  supxrge  45288  uzn0bi  45409  elprn1  45589  elprn2  45590  liminflbuz2  45771  itgcoscmulx  45925  fourierdlem41  46104  elaa2  46190  sge0cl  46337  meadjiunlem  46421  hoidmvlelem2  46552  hspmbllem1  46582