Theorem neii 2927

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  nesymi  2982  nemtbir  3021  snsssn  4795  nlim1  8414  nlim2  8415  2dom  8962  map2xp  9071  snnen2o  9144  ssttrcl  9630  ttrclselem2  9641  updjudhcoinrg  9848  pm54.43lem  9915  canthp1lem2  10566  ine0  11573  xrltnr  13039  pnfnlt  13048  prprrab  14398  tpf1ofv1  14422  tpf1ofv2  14423  wrdlen2i  14867  3lcm2e6woprm  16544  6lcm4e12  16545  m1dvdsndvds  16728  fnpr2ob  17480  fvprif  17483  pmatcollpw3fi1lem1  22689  sinhalfpilem  26388  coseq1  26450  2lgslem3  27331  2lgslem4  27333  sltval2  27584  nosgnn0  27586  sltintdifex  27589  sltres  27590  sltsolem1  27603  nolt02o  27623  nogt01o  27624  axlowdimlem13  28917  axlowdim1  28922  umgredgnlp  29110  wwlksnext  29856  norm1exi  31212  largei  32229  sgnnbi  32796  sgnpbi  32797  ind1a  32815  rtelextdg2lem  33692  2sqr3minply  33746  2sqr3nconstr  33747  cos9thpinconstrlem2  33756  ballotlemii  34471  gonanegoal  35324  gonan0  35364  goaln0  35365  fmlasucdisj  35371  ex-sategoelelomsuc  35398  ex-sategoelel12  35399  dfrdg2  35768  dfrdg4  35924  bj-1nel0  36927  bj-pr21val  36986  finxpreclem2  37363  epnsymrel  38538  0dioph  42751  oaomoencom  43290  clsk1indlem1  44018  dirkercncflem2  46086  fourierdlem60  46148  fourierdlem61  46149  afv20defat  47217  fun2dmnopgexmpl  47269  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  itcoval1  48649  line2ylem  48737  fucofvalne  49311