Theorem neneq 2931

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon3ad  2938  necon3ai  2950  2reu4lem  4481  pr1eqbg  4817  fpropnf1  7224  nf1const  7261  nelaneq  9528  gcd2n0cl  16455  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  ncoprmgcdne1b  16596  isnsgrp  18632  isnmnd  18647  mulmarep1gsum1  22493  fvmptnn04ifb  22771  tdeglem4  25998  isosctrlem2  26762  nnsge1  28275  structiedg0val  29002  umgr2edgneu  29194  imadifxp  32580  f1resrcmplf1dlem  35069  aks6d1c2p2  42100  xppss12  42210  n0p  45032  supxrge  45327  uzn0bi  45448  elprn1  45624  elprn2  45625  liminflbuz2  45806  itgcoscmulx  45960  fourierdlem41  46139  elaa2  46225  sge0cl  46372  meadjiunlem  46456  hoidmvlelem2  46587  hspmbllem1  46617