Theorem neii 2959

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

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

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 2958

This theorem is used by:  nesymi  3014  nemtbir  3053  snsssn  4804  nlim1  8480  nlim2  8481  2dom  9041  map2xp  9149  snnen2o  9219  ssttrcl  9698  ttrclselem2  9709  updjudhcoinrg  9942  pm54.43lem  10009  canthp1lem2  10666  ine0  11677  ind1a  12257  xrltnr  13174  pnfnlt  13183  prprrab  14542  tpf1ofv1  14566  tpf1ofv2  14567  wrdlen2i  15017  sgnnbi  15181  sgnpbi  15182  3lcm2e6woprm  16711  6lcm4e12  16712  m1dvdsndvds  16896  fnpr2ob  17650  fvprif  17653  pmatcollpw3fi1lem1  23017  sinhalfpilem  26708  coseq1  26770  2lgslem3  27648  2lgslem4  27650  ltsval2  27900  nosgnn0  27902  ltsintdifex  27905  ltsres  27906  ltssolem1  27919  nolt02o  27939  nogt01o  27940  axlowdimlem13  29419  axlowdim1  29424  umgredgnlp  29612  wwlksnext  30369  norm1exi  31739  largei  32756  rtelextdg2lem  34244  2sqr3minply  34298  2sqr3nconstr  34299  cos9thpinconstrlem2  34308  ballotlemii  35023  gonanegoal  35939  gonan0  35979  goaln0  35980  fmlasucdisj  35986  ex-sategoelelomsuc  36013  ex-sategoelel12  36014  dfrdg2  36380  dfrdg4  36538  bj-1nel0  37706  bj-pr21val  37765  finxpreclem2  38152  epnsymrel  39402  0dioph  43631  oaomoencom  44166  clsk1indlem1  44893  dirkercncflem2  46940  fourierdlem60  47002  fourierdlem61  47003  goldratmolem4  47761  afv20defat  48128  fun2dmnopgexmpl  48180  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  itcoval1  49601  line2ylem  49689  fucofvalne  50259