Theorem neneq 2990

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1522   ≠ wne 2984

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 208  df-ne 2985

This theorem is referenced by:  necon3ad  2997  2reu4lem  4379  pr1eqbg  4694  fpropnf1  6890  nelaneq  8909  gcd2n0cl  15691  lcmfunsnlem2lem1  15811  lcmfunsnlem2lem2  15812  ncoprmgcdne1b  15823  isnsgrp  17727  isnmnd  17737  mulmarep1gsum1  20866  fvmptnn04ifb  21143  isosctrlem2  25078  structiedg0val  26490  umgr2edgneu  26679  imadifxp  30041  f1resrcmplf1dlem  31973  xppss12  38645  n0p  40844  supxrge  41147  uzn0bi  41277  elprn1  41456  elprn2  41457  liminflbuz2  41638  itgcoscmulx  41795  fourierdlem41  41975  elaa2  42061  sge0cl  42205  meadjiunlem  42289  hoidmvlelem2  42420  hspmbllem1  42450