Theorem neii 3018

Description: Inference associated with df-ne 3017. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neii.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
neii	⊢ ¬ 𝐴 = 𝐵

Proof of Theorem neii

Step	Hyp	Ref	Expression
1		neii.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		df-ne 3017	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 232	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = wceq 1533   ≠ wne 3016

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 3017

This theorem is referenced by:  nesymi  3073  nemtbir  3112  snsssn  4765  2dom  8576  map2xp  8681  updjudhcoinrg  9356  pm54.43lem  9422  canthp1lem2  10069  ine0  11069  inelr  11622  xrltnr  12508  pnfnlt  12517  prprrab  13825  wrdlen2i  14298  3lcm2e6woprm  15953  6lcm4e12  15954  m1dvdsndvds  16129  fnpr2ob  16825  fvprif  16828  pmatcollpw3fi1lem1  21388  sinhalfpilem  25043  coseq1  25104  2lgslem3  25974  2lgslem4  25976  axlowdimlem13  26734  axlowdim1  26739  umgredgnlp  26926  wwlksnext  27665  norm1exi  29021  largei  30038  ind1a  31273  ballotlemii  31756  sgnnbi  31798  sgnpbi  31799  gonanegoal  32594  gonan0  32634  goaln0  32635  fmlasucdisj  32641  ex-sategoelelomsuc  32668  ex-sategoelel12  32669  dfrdg2  33035  sltval2  33158  nosgnn0  33160  sltintdifex  33163  sltres  33164  sltsolem1  33175  nolt02o  33194  dfrdg4  33407  bj-1nel0  34261  bj-pr21val  34320  finxpreclem2  34665  epnsymrel  35792  0dioph  39368  clsk1indlem1  40388  dirkercncflem2  42383  fourierdlem60  42445  fourierdlem61  42446  afv20defat  43425  fun2dmnopgexmpl  43477  line2ylem  44732