Theorem neii 2957

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  nesymi  3012  nemtbir  3051  snsssn  4800  nlim1  8497  nlim2  8498  2dom  9058  map2xp  9166  snnen2o  9236  ssttrcl  9716  ttrclselem2  9727  updjudhcoinrg  10014  pm54.43lem  10081  canthp1lem2  10738  ine0  11751  ind1a  12331  xrltnr  13248  pnfnlt  13257  prprrab  14618  tpf1ofv1  14642  tpf1ofv2  14643  wrdlen2i  15093  sgnnbi  15257  sgnpbi  15258  3lcm2e6woprm  16790  6lcm4e12  16791  m1dvdsndvds  16976  fnpr2ob  17730  fvprif  17733  pmatcollpw3fi1lem1  23104  sinhalfpilem  26792  coseq1  26853  2lgslem3  27731  2lgslem4  27733  ltsval2  28013  nosgnn0  28015  ltsintdifex  28018  ltsres  28019  ltssolem1  28032  nolt02o  28052  nogt01o  28053  axlowdimlem13  29532  axlowdim1  29537  umgredgnlp  29725  wwlksnext  30482  norm1exi  31852  largei  32869  rtelextdg2lem  34400  2sqr3minply  34454  2sqr3nconstr  34455  cos9thpinconstrlem2  34464  ballotlemii  35178  gonanegoal  36159  gonan0  36199  goaln0  36200  fmlasucdisj  36206  ex-sategoelelomsuc  36233  ex-sategoelel12  36234  dfrdg2  36599  dfrdg4  36757  bj-1nel0  37909  bj-pr21val  37968  finxpreclem2  38356  epnsymrel  39621  0dioph  43832  oaomoencom  44362  clsk1indlem1  45088  dirkercncflem2  47157  fourierdlem60  47219  fourierdlem61  47220  goldratmolem4  47978  afv20defat  48345  fun2dmnopgexmpl  48397  usgrexmpl2nb0  49172  usgrexmpl2nb1  49173  usgrexmpl2nb2  49174  usgrexmpl2nb3  49175  usgrexmpl2nb4  49176  usgrexmpl2nb5  49177  itcoval1  49818  line2ylem  49906  fucofvalne  50476