Theorem neii 2940

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

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  nesymi  2996  nemtbir  3036  snsssn  4843  nlim1  8493  nlim2  8494  2dom  9034  map2xp  9151  snnen2o  9241  ssttrcl  9714  ttrclselem2  9725  updjudhcoinrg  9932  pm54.43lem  9999  canthp1lem2  10652  ine0  11655  inelr  12208  xrltnr  13105  pnfnlt  13114  prprrab  14440  wrdlen2i  14899  3lcm2e6woprm  16558  6lcm4e12  16559  m1dvdsndvds  16737  fnpr2ob  17510  fvprif  17513  pmatcollpw3fi1lem1  22510  sinhalfpilem  26207  coseq1  26268  2lgslem3  27141  2lgslem4  27143  sltval2  27393  nosgnn0  27395  sltintdifex  27398  sltres  27399  sltsolem1  27412  nolt02o  27432  nogt01o  27433  axlowdimlem13  28477  axlowdim1  28482  umgredgnlp  28672  wwlksnext  29412  norm1exi  30768  largei  31785  ind1a  33313  ballotlemii  33798  sgnnbi  33840  sgnpbi  33841  gonanegoal  34639  gonan0  34679  goaln0  34680  fmlasucdisj  34686  ex-sategoelelomsuc  34713  ex-sategoelel12  34714  dfrdg2  35069  dfrdg4  35225  bj-1nel0  36140  bj-pr21val  36199  finxpreclem2  36576  epnsymrel  37737  sn-inelr  41642  0dioph  41820  oaomoencom  42371  clsk1indlem1  43100  dirkercncflem2  45120  fourierdlem60  45182  fourierdlem61  45183  afv20defat  46240  fun2dmnopgexmpl  46292  itcoval1  47438  line2ylem  47526