Theorem neneq 2939

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

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

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 2934

This theorem is referenced by:  necon3ad  2946  necon3ai  2958  2reu4lem  4502  pr1eqbg  4838  fpropnf1  7265  nf1const  7302  nelaneq  9618  gcd2n0cl  16533  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  ncoprmgcdne1b  16674  isnsgrp  18706  isnmnd  18721  mulmarep1gsum1  22516  fvmptnn04ifb  22794  tdeglem4  26022  isosctrlem2  26786  nnsge1  28292  structiedg0val  29006  umgr2edgneu  29198  imadifxp  32587  f1resrcmplf1dlem  35122  aks6d1c2p2  42137  xppss12  42247  n0p  45036  supxrge  45332  uzn0bi  45453  elprn1  45629  elprn2  45630  liminflbuz2  45811  itgcoscmulx  45965  fourierdlem41  46144  elaa2  46230  sge0cl  46377  meadjiunlem  46461  hoidmvlelem2  46592  hspmbllem1  46622