Theorem neii 2930

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

Syntax hints:  ¬ wn 3   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  nesymi  2985  nemtbir  3024  snsssn  4793  nlim1  8404  nlim2  8405  2dom  8952  map2xp  9060  snnen2o  9129  ssttrcl  9605  ttrclselem2  9616  updjudhcoinrg  9826  pm54.43lem  9893  canthp1lem2  10544  ine0  11552  xrltnr  13018  pnfnlt  13027  prprrab  14380  tpf1ofv1  14404  tpf1ofv2  14405  wrdlen2i  14849  3lcm2e6woprm  16526  6lcm4e12  16527  m1dvdsndvds  16710  fnpr2ob  17462  fvprif  17465  pmatcollpw3fi1lem1  22702  sinhalfpilem  26400  coseq1  26462  2lgslem3  27343  2lgslem4  27345  sltval2  27596  nosgnn0  27598  sltintdifex  27601  sltres  27602  sltsolem1  27615  nolt02o  27635  nogt01o  27636  axlowdimlem13  28933  axlowdim1  28938  umgredgnlp  29126  wwlksnext  29872  norm1exi  31228  largei  32245  sgnnbi  32819  sgnpbi  32820  ind1a  32838  rtelextdg2lem  33737  2sqr3minply  33791  2sqr3nconstr  33792  cos9thpinconstrlem2  33801  ballotlemii  34515  gonanegoal  35394  gonan0  35434  goaln0  35435  fmlasucdisj  35441  ex-sategoelelomsuc  35468  ex-sategoelel12  35469  dfrdg2  35835  dfrdg4  35991  bj-1nel0  36994  bj-pr21val  37053  finxpreclem2  37430  epnsymrel  38605  0dioph  42817  oaomoencom  43356  clsk1indlem1  44084  dirkercncflem2  46148  fourierdlem60  46210  fourierdlem61  46211  afv20defat  47269  fun2dmnopgexmpl  47321  usgrexmpl2nb0  48068  usgrexmpl2nb1  48069  usgrexmpl2nb2  48070  usgrexmpl2nb3  48071  usgrexmpl2nb4  48072  usgrexmpl2nb5  48073  itcoval1  48701  line2ylem  48789  fucofvalne  49363