Theorem neneq 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  necon3ad  2954  necon3ai  2966  2reu4lem  4526  pr1eqbg  4858  disjprgw  5144  fpropnf1  7266  nf1const  7302  nelaneq  9594  gcd2n0cl  16450  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  ncoprmgcdne1b  16587  isnsgrp  18614  isnmnd  18629  mulmarep1gsum1  22075  fvmptnn04ifb  22353  tdeglem4  25577  isosctrlem2  26324  structiedg0val  28282  umgr2edgneu  28471  imadifxp  31832  f1resrcmplf1dlem  34089  aks6d1c2p2  40957  xppss12  41047  n0p  43730  supxrge  44048  uzn0bi  44169  elprn1  44349  elprn2  44350  liminflbuz2  44531  itgcoscmulx  44685  fourierdlem41  44864  elaa2  44950  sge0cl  45097  meadjiunlem  45181  hoidmvlelem2  45312  hspmbllem1  45342