Theorem neii 2927

Description: Inference associated with df-ne 2926. (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 2926	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 230	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = 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:  nesymi  2982  nemtbir  3021  snsssn  4805  nlim1  8453  nlim2  8454  2dom  9001  map2xp  9111  snnen2o  9184  ssttrcl  9668  ttrclselem2  9679  updjudhcoinrg  9886  pm54.43lem  9953  canthp1lem2  10606  ine0  11613  xrltnr  13079  pnfnlt  13088  prprrab  14438  tpf1ofv1  14462  tpf1ofv2  14463  wrdlen2i  14908  3lcm2e6woprm  16585  6lcm4e12  16586  m1dvdsndvds  16769  fnpr2ob  17521  fvprif  17524  pmatcollpw3fi1lem1  22673  sinhalfpilem  26372  coseq1  26434  2lgslem3  27315  2lgslem4  27317  sltval2  27568  nosgnn0  27570  sltintdifex  27573  sltres  27574  sltsolem1  27587  nolt02o  27607  nogt01o  27608  axlowdimlem13  28881  axlowdim1  28886  umgredgnlp  29074  wwlksnext  29823  norm1exi  31179  largei  32196  sgnnbi  32763  sgnpbi  32764  ind1a  32782  rtelextdg2lem  33716  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpinconstrlem2  33780  ballotlemii  34495  gonanegoal  35339  gonan0  35379  goaln0  35380  fmlasucdisj  35386  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  dfrdg2  35783  dfrdg4  35939  bj-1nel0  36942  bj-pr21val  37001  finxpreclem2  37378  epnsymrel  38553  0dioph  42766  oaomoencom  43306  clsk1indlem1  44034  dirkercncflem2  46102  fourierdlem60  46164  fourierdlem61  46165  afv20defat  47230  fun2dmnopgexmpl  47282  usgrexmpl2nb0  48019  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  itcoval1  48649  line2ylem  48737  fucofvalne  49311