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 229	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = wceq 1533   ≠ 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 206  df-ne 2930

This theorem is referenced by:  nesymi  2987  nemtbir  3027  snsssn  4844  nlim1  8510  nlim2  8511  2dom  9055  map2xp  9172  snnen2o  9262  ssttrcl  9740  ttrclselem2  9751  updjudhcoinrg  9958  pm54.43lem  10025  canthp1lem2  10678  ine0  11681  inelr  12235  xrltnr  13134  pnfnlt  13143  prprrab  14470  wrdlen2i  14929  3lcm2e6woprm  16589  6lcm4e12  16590  m1dvdsndvds  16770  fnpr2ob  17543  fvprif  17546  pmatcollpw3fi1lem1  22732  sinhalfpilem  26443  coseq1  26504  2lgslem3  27382  2lgslem4  27384  sltval2  27635  nosgnn0  27637  sltintdifex  27640  sltres  27641  sltsolem1  27654  nolt02o  27674  nogt01o  27675  axlowdimlem13  28837  axlowdim1  28842  umgredgnlp  29032  wwlksnext  29776  norm1exi  31132  largei  32149  ind1a  33769  ballotlemii  34254  sgnnbi  34296  sgnpbi  34297  gonanegoal  35093  gonan0  35133  goaln0  35134  fmlasucdisj  35140  ex-sategoelelomsuc  35167  ex-sategoelel12  35168  dfrdg2  35522  dfrdg4  35678  bj-1nel0  36564  bj-pr21val  36623  finxpreclem2  37000  epnsymrel  38164  sn-inelr  42155  0dioph  42340  oaomoencom  42888  clsk1indlem1  43617  dirkercncflem2  45630  fourierdlem60  45692  fourierdlem61  45693  afv20defat  46750  fun2dmnopgexmpl  46802  itcoval1  47922  line2ylem  48010