Theorem neneq 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon3ad  2946  necon3ai  2958  2reu4lem  4464  elprn1  4596  elprn2  4597  pr1eqbg  4801  fpropnf1  7216  nf1const  7253  nelaneqOLDOLD  9512  gcd2n0cl  16472  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  ncoprmgcdne1b  16613  isnsgrp  18685  isnmnd  18700  mulmarep1gsum1  22551  fvmptnn04ifb  22829  tdeglem4  26038  isosctrlem2  26799  nnsge1  28352  structiedg0val  29108  umgr2edgneu  29300  imadifxp  32689  f1resrcmplf1dlem  35248  elttcirr  36732  aks6d1c2p2  42575  xppss12  42687  n0p  45497  supxrge  45789  uzn0bi  45908  liminflbuz2  46264  itgcoscmulx  46418  fourierdlem41  46597  elaa2  46683  sge0cl  46830  meadjiunlem  46914  hoidmvlelem2  47045  hspmbllem1  47075  chnerlem1  47331