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 1537   ≠ 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  4772  2dom  8582  map2xp  8687  updjudhcoinrg  9362  pm54.43lem  9428  canthp1lem2  10075  ine0  11075  inelr  11628  xrltnr  12515  pnfnlt  12524  prprrab  13832  wrdlen2i  14304  3lcm2e6woprm  15959  6lcm4e12  15960  m1dvdsndvds  16135  fnpr2ob  16831  fvprif  16834  pmatcollpw3fi1lem1  21394  sinhalfpilem  25049  coseq1  25110  2lgslem3  25980  2lgslem4  25982  axlowdimlem13  26740  axlowdim1  26745  umgredgnlp  26932  wwlksnext  27671  norm1exi  29027  largei  30044  ind1a  31278  ballotlemii  31761  sgnnbi  31803  sgnpbi  31804  gonanegoal  32599  gonan0  32639  goaln0  32640  fmlasucdisj  32646  ex-sategoelelomsuc  32673  ex-sategoelel12  32674  dfrdg2  33040  sltval2  33163  nosgnn0  33165  sltintdifex  33168  sltres  33169  sltsolem1  33180  nolt02o  33199  dfrdg4  33412  bj-1nel0  34269  bj-pr21val  34328  finxpreclem2  34674  epnsymrel  35813  0dioph  39395  clsk1indlem1  40415  dirkercncflem2  42409  fourierdlem60  42471  fourierdlem61  42472  afv20defat  43451  fun2dmnopgexmpl  43503  line2ylem  44758