Theorem neii 2958

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2956

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 2957

This theorem is used by:  nesymi  3013  nemtbir  3052  snsssn  4801  nlim1  8481  nlim2  8482  2dom  9042  map2xp  9150  snnen2o  9220  ssttrcl  9700  ttrclselem2  9711  updjudhcoinrg  9995  pm54.43lem  10062  canthp1lem2  10719  ine0  11732  ind1a  12312  xrltnr  13229  pnfnlt  13238  prprrab  14598  tpf1ofv1  14622  tpf1ofv2  14623  wrdlen2i  15073  sgnnbi  15237  sgnpbi  15238  3lcm2e6woprm  16770  6lcm4e12  16771  m1dvdsndvds  16956  fnpr2ob  17710  fvprif  17713  pmatcollpw3fi1lem1  23084  sinhalfpilem  26774  coseq1  26835  2lgslem3  27713  2lgslem4  27715  ltsval2  27995  nosgnn0  27997  ltsintdifex  28000  ltsres  28001  ltssolem1  28014  nolt02o  28034  nogt01o  28035  axlowdimlem13  29514  axlowdim1  29519  umgredgnlp  29707  wwlksnext  30464  norm1exi  31834  largei  32851  rtelextdg2lem  34340  2sqr3minply  34394  2sqr3nconstr  34395  cos9thpinconstrlem2  34404  ballotlemii  35119  gonanegoal  36086  gonan0  36126  goaln0  36127  fmlasucdisj  36133  ex-sategoelelomsuc  36160  ex-sategoelel12  36161  dfrdg2  36527  dfrdg4  36685  bj-1nel0  37837  bj-pr21val  37896  finxpreclem2  38281  epnsymrel  39546  0dioph  43742  oaomoencom  44277  clsk1indlem1  45004  dirkercncflem2  47058  fourierdlem60  47120  fourierdlem61  47121  goldratmolem4  47879  afv20defat  48246  fun2dmnopgexmpl  48298  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  itcoval1  49719  line2ylem  49807  fucofvalne  50377