Theorem neneq 2829

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon3ad  2836  pr1eqbg  4421  fpropnf1  6564  mpt2difsnif  6795  hash2prd  13295  fprodn0f  14766  gcd2n0cl  15278  lcmfunsnlem2lem1  15398  isnsgrp  17335  isnmnd  17345  structiedg0val  25956  umgr2edgneu  26151  clwwlknclwwlkdifsOLD  26947  numclwwlk3lemOLD  27369  n0p  39523  supxrge  39867  uzn0bi  40002  elprn1  40183  elprn2  40184  itgcoscmulx  40503  fourierdlem41  40683  elaa2  40769  sge0cl  40916  meadjiunlem  41000  hoidmvlelem2  41131  hspmbllem1  41161  2reu4a  41510  fdmdifeqresdif  42445