Theorem neii 2934

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

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

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 2933

This theorem is referenced by:  nesymi  2989  nemtbir  3028  snsssn  4797  nlim1  8416  nlim2  8417  2dom  8967  map2xp  9075  snnen2o  9145  ssttrcl  9624  ttrclselem2  9635  updjudhcoinrg  9845  pm54.43lem  9912  canthp1lem2  10564  ine0  11572  xrltnr  13033  pnfnlt  13042  prprrab  14396  tpf1ofv1  14420  tpf1ofv2  14421  wrdlen2i  14865  3lcm2e6woprm  16542  6lcm4e12  16543  m1dvdsndvds  16726  fnpr2ob  17479  fvprif  17482  pmatcollpw3fi1lem1  22730  sinhalfpilem  26428  coseq1  26490  2lgslem3  27371  2lgslem4  27373  ltsval2  27624  nosgnn0  27626  ltsintdifex  27629  ltsres  27630  ltssolem1  27643  nolt02o  27663  nogt01o  27664  axlowdimlem13  29027  axlowdim1  29032  umgredgnlp  29220  wwlksnext  29966  norm1exi  31325  largei  32342  sgnnbi  32919  sgnpbi  32920  ind1a  32938  rtelextdg2lem  33883  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpinconstrlem2  33947  ballotlemii  34661  gonanegoal  35546  gonan0  35586  goaln0  35587  fmlasucdisj  35593  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  dfrdg2  35987  dfrdg4  36145  bj-1nel0  37155  bj-pr21val  37214  finxpreclem2  37591  epnsymrel  38815  0dioph  43016  oaomoencom  43555  clsk1indlem1  44282  dirkercncflem2  46344  fourierdlem60  46406  fourierdlem61  46407  afv20defat  47474  fun2dmnopgexmpl  47526  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  itcoval1  48905  line2ylem  48993  fucofvalne  49566