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  4473  pr1eqbg  4808  fpropnf1  7204  nf1const  7241  nelaneqOLD  9494  gcd2n0cl  16420  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  ncoprmgcdne1b  16561  isnsgrp  18597  isnmnd  18612  mulmarep1gsum1  22458  fvmptnn04ifb  22736  tdeglem4  25963  isosctrlem2  26727  nnsge1  28240  structiedg0val  28967  umgr2edgneu  29159  imadifxp  32545  f1resrcmplf1dlem  35053  aks6d1c2p2  42096  xppss12  42206  n0p  45027  supxrge  45322  uzn0bi  45442  elprn1  45618  elprn2  45619  liminflbuz2  45800  itgcoscmulx  45954  fourierdlem41  46133  elaa2  46219  sge0cl  46366  meadjiunlem  46450  hoidmvlelem2  46581  hspmbllem1  46611