Theorem neii 2934

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ 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:  nesymi  2989  nemtbir  3028  snsssn  4817  nlim1  8499  nlim2  8500  2dom  9042  map2xp  9159  snnen2o  9243  ssttrcl  9727  ttrclselem2  9738  updjudhcoinrg  9945  pm54.43lem  10012  canthp1lem2  10665  ine0  11670  inelr  12228  xrltnr  13133  pnfnlt  13142  prprrab  14489  tpf1ofv1  14513  tpf1ofv2  14514  wrdlen2i  14959  3lcm2e6woprm  16632  6lcm4e12  16633  m1dvdsndvds  16816  fnpr2ob  17570  fvprif  17573  pmatcollpw3fi1lem1  22722  sinhalfpilem  26422  coseq1  26484  2lgslem3  27365  2lgslem4  27367  sltval2  27618  nosgnn0  27620  sltintdifex  27623  sltres  27624  sltsolem1  27637  nolt02o  27657  nogt01o  27658  axlowdimlem13  28879  axlowdim1  28884  umgredgnlp  29072  wwlksnext  29821  norm1exi  31177  largei  32194  sgnnbi  32763  sgnpbi  32764  ind1a  32782  rtelextdg2lem  33706  2sqr3minply  33760  2sqr3nconstr  33761  ballotlemii  34482  gonanegoal  35320  gonan0  35360  goaln0  35361  fmlasucdisj  35367  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  dfrdg2  35759  dfrdg4  35915  bj-1nel0  36918  bj-pr21val  36977  finxpreclem2  37354  epnsymrel  38526  sn-inelr  42457  0dioph  42748  oaomoencom  43288  clsk1indlem1  44016  dirkercncflem2  46081  fourierdlem60  46143  fourierdlem61  46144  afv20defat  47209  fun2dmnopgexmpl  47261  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  itcoval1  48591  line2ylem  48679  fucofvalne  49184