Theorem neneq 2931

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon3ad  2938  necon3ai  2950  2reu4lem  4485  pr1eqbg  4821  fpropnf1  7242  nf1const  7279  nelaneq  9552  gcd2n0cl  16479  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  ncoprmgcdne1b  16620  isnsgrp  18650  isnmnd  18665  mulmarep1gsum1  22460  fvmptnn04ifb  22738  tdeglem4  25965  isosctrlem2  26729  nnsge1  28235  structiedg0val  28949  umgr2edgneu  29141  imadifxp  32530  f1resrcmplf1dlem  35076  aks6d1c2p2  42107  xppss12  42217  n0p  45039  supxrge  45334  uzn0bi  45455  elprn1  45631  elprn2  45632  liminflbuz2  45813  itgcoscmulx  45967  fourierdlem41  46146  elaa2  46232  sge0cl  46379  meadjiunlem  46463  hoidmvlelem2  46594  hspmbllem1  46624