Theorem neneq 2952

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

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

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 2947

This theorem is referenced by:  necon3ad  2959  necon3ai  2971  2reu4lem  4545  pr1eqbg  4881  fpropnf1  7304  nf1const  7340  nelaneq  9668  gcd2n0cl  16555  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  ncoprmgcdne1b  16697  isnsgrp  18761  isnmnd  18776  mulmarep1gsum1  22600  fvmptnn04ifb  22878  tdeglem4  26119  isosctrlem2  26880  nnsge1  28364  structiedg0val  29057  umgr2edgneu  29249  imadifxp  32623  f1resrcmplf1dlem  35062  aks6d1c2p2  42076  xppss12  42222  n0p  44945  supxrge  45253  uzn0bi  45374  elprn1  45554  elprn2  45555  liminflbuz2  45736  itgcoscmulx  45890  fourierdlem41  46069  elaa2  46155  sge0cl  46302  meadjiunlem  46386  hoidmvlelem2  46517  hspmbllem1  46547