Theorem neii 2960

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

Syntax hints:  ¬ wn 3   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  nesymi  3015  nemtbir  3054  snsssn  4807  nlim1  8475  nlim2  8476  2dom  9028  map2xp  9136  snnen2o  9206  ssttrcl  9685  ttrclselem2  9696  updjudhcoinrg  9920  pm54.43lem  9987  canthp1lem2  10639  ine0  11650  ind1a  12230  xrltnr  13145  pnfnlt  13154  prprrab  14512  tpf1ofv1  14536  tpf1ofv2  14537  wrdlen2i  14981  sgnnbi  15143  sgnpbi  15144  3lcm2e6woprm  16674  6lcm4e12  16675  m1dvdsndvds  16859  fnpr2ob  17613  fvprif  17616  pmatcollpw3fi1lem1  22924  sinhalfpilem  26606  coseq1  26668  2lgslem3  27546  2lgslem4  27548  ltsval2  27798  nosgnn0  27800  ltsintdifex  27803  ltsres  27804  ltssolem1  27817  nolt02o  27837  nogt01o  27838  axlowdimlem13  29282  axlowdim1  29287  umgredgnlp  29475  wwlksnext  30220  norm1exi  31580  largei  32597  rtelextdg2lem  34094  2sqr3minply  34148  2sqr3nconstr  34149  cos9thpinconstrlem2  34158  ballotlemii  34872  gonanegoal  35822  gonan0  35862  goaln0  35863  fmlasucdisj  35869  ex-sategoelelomsuc  35896  ex-sategoelel12  35897  dfrdg2  36263  dfrdg4  36421  bj-1nel0  37568  bj-pr21val  37627  finxpreclem2  38014  epnsymrel  39273  0dioph  43489  oaomoencom  44024  clsk1indlem1  44751  dirkercncflem2  46798  fourierdlem60  46860  fourierdlem61  46861  afv20defat  47946  fun2dmnopgexmpl  47998  usgrexmpl2nb0  48773  usgrexmpl2nb1  48774  usgrexmpl2nb2  48775  usgrexmpl2nb3  48776  usgrexmpl2nb4  48777  usgrexmpl2nb5  48778  itcoval1  49420  line2ylem  49508  fucofvalne  50080