Theorem neneq 3024

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon3ad  3031  2reu4lem  4467  pr1eqbg  4789  disjprgw  5063  fpropnf1  7027  nf1const  7061  nelaneq  9065  gcd2n0cl  15860  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  ncoprmgcdne1b  15996  isnsgrp  17907  isnmnd  17917  mulmarep1gsum1  21184  fvmptnn04ifb  21461  isosctrlem2  25399  structiedg0val  26809  umgr2edgneu  26998  imadifxp  30353  f1resrcmplf1dlem  32361  xppss12  39122  n0p  41312  supxrge  41613  uzn0bi  41742  elprn1  41921  elprn2  41922  liminflbuz2  42103  itgcoscmulx  42261  fourierdlem41  42440  elaa2  42526  sge0cl  42670  meadjiunlem  42754  hoidmvlelem2  42885  hspmbllem1  42915