Theorem neii 2931

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

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

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 2930

This theorem is referenced by:  nesymi  2986  nemtbir  3025  snsssn  4792  nlim1  8410  nlim2  8411  2dom  8959  map2xp  9067  snnen2o  9136  ssttrcl  9612  ttrclselem2  9623  updjudhcoinrg  9833  pm54.43lem  9900  canthp1lem2  10551  ine0  11559  xrltnr  13020  pnfnlt  13029  prprrab  14382  tpf1ofv1  14406  tpf1ofv2  14407  wrdlen2i  14851  3lcm2e6woprm  16528  6lcm4e12  16529  m1dvdsndvds  16712  fnpr2ob  17464  fvprif  17467  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  28934  axlowdim1  28939  umgredgnlp  29127  wwlksnext  29873  norm1exi  31232  largei  32249  sgnnbi  32826  sgnpbi  32827  ind1a  32845  rtelextdg2lem  33760  2sqr3minply  33814  2sqr3nconstr  33815  cos9thpinconstrlem2  33824  ballotlemii  34538  gonanegoal  35417  gonan0  35457  goaln0  35458  fmlasucdisj  35464  ex-sategoelelomsuc  35491  ex-sategoelel12  35492  dfrdg2  35858  dfrdg4  36016  bj-1nel0  37019  bj-pr21val  37078  finxpreclem2  37455  epnsymrel  38679  0dioph  42896  oaomoencom  43435  clsk1indlem1  44163  dirkercncflem2  46227  fourierdlem60  46289  fourierdlem61  46290  afv20defat  47357  fun2dmnopgexmpl  47409  usgrexmpl2nb0  48156  usgrexmpl2nb1  48157  usgrexmpl2nb2  48158  usgrexmpl2nb3  48159  usgrexmpl2nb4  48160  usgrexmpl2nb5  48161  itcoval1  48789  line2ylem  48877  fucofvalne  49451