Theorem neneq 2938

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

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

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 2933

This theorem is referenced by:  necon3ad  2945  necon3ai  2957  2reu4lem  4463  elprn1  4595  elprn2  4596  pr1eqbg  4800  fpropnf1  7222  nf1const  7259  nelaneqOLDOLD  9518  gcd2n0cl  16478  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  ncoprmgcdne1b  16619  isnsgrp  18691  isnmnd  18706  mulmarep1gsum1  22538  fvmptnn04ifb  22816  tdeglem4  26025  isosctrlem2  26783  nnsge1  28335  structiedg0val  29091  umgr2edgneu  29283  imadifxp  32671  f1resrcmplf1dlem  35229  elttcirr  36713  aks6d1c2p2  42558  xppss12  42670  n0p  45476  supxrge  45768  uzn0bi  45887  liminflbuz2  46243  itgcoscmulx  46397  fourierdlem41  46576  elaa2  46662  sge0cl  46809  meadjiunlem  46893  hoidmvlelem2  47024  hspmbllem1  47054  chnerlem1  47312