Theorem neii 2961

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

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

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 2960

This theorem is used by:  nesymi  3016  nemtbir  3055  snsssn  4799  nlim1  8525  nlim2  8526  2dom  9086  map2xp  9194  snnen2o  9264  ssttrcl  9743  ttrclselem2  9754  updjudhcoinrg  10041  pm54.43lem  10108  canthp1lem2  10765  ine0  11778  ind1a  12358  xrltnr  13275  pnfnlt  13284  prprrab  14645  tpf1ofv1  14669  tpf1ofv2  14670  wrdlen2i  15122  sgnnbi  15286  sgnpbi  15287  3lcm2e6woprm  16819  6lcm4e12  16820  m1dvdsndvds  17005  fnpr2ob  17759  fvprif  17762  pmatcollpw3fi1lem1  23134  sinhalfpilem  26822  coseq1  26883  2lgslem3  27761  2lgslem4  27763  ltsval2  28043  nosgnn0  28045  ltsintdifex  28048  ltsres  28049  ltssolem1  28062  nolt02o  28082  nogt01o  28083  axlowdimlem13  29562  axlowdim1  29567  umgredgnlp  29755  wwlksnext  30512  norm1exi  31882  largei  32899  rtelextdg2lem  34428  2sqr3minply  34482  2sqr3nconstr  34483  cos9thpinconstrlem2  34492  ballotlemii  35206  gonanegoal  36284  gonan0  36324  goaln0  36325  fmlasucdisj  36331  ex-sategoelelomsuc  36358  ex-sategoelel12  36359  dfrdg2  36735  dfrdg4  36893  bj-1nel0  38045  bj-pr21val  38104  finxpreclem2  38505  epnsymrel  39770  0dioph  43982  oaomoencom  44511  clsk1indlem1  45237  dirkercncflem2  47319  fourierdlem60  47381  fourierdlem61  47382  goldratmolem4  48140  afv20defat  48507  fun2dmnopgexmpl  48559  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336  usgrexmpl2nb3  49337  usgrexmpl2nb4  49338  usgrexmpl2nb5  49339  itcoval1  49980  line2ylem  50068  fucofvalne  50652  parhomeqor2  50963  par2hom  50984