Theorem neii 2989

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

Syntax hints:  ¬ wn 3   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  nesymi  3044  nemtbir  3082  snsssn  4732  2dom  8565  map2xp  8671  updjudhcoinrg  9346  pm54.43lem  9413  canthp1lem2  10064  ine0  11064  inelr  11615  xrltnr  12502  pnfnlt  12511  prprrab  13827  wrdlen2i  14295  3lcm2e6woprm  15949  6lcm4e12  15950  m1dvdsndvds  16125  fnpr2ob  16823  fvprif  16826  pmatcollpw3fi1lem1  21391  sinhalfpilem  25056  coseq1  25117  2lgslem3  25988  2lgslem4  25990  axlowdimlem13  26748  axlowdim1  26753  umgredgnlp  26940  wwlksnext  27679  norm1exi  29033  largei  30050  ind1a  31388  ballotlemii  31871  sgnnbi  31913  sgnpbi  31914  gonanegoal  32712  gonan0  32752  goaln0  32753  fmlasucdisj  32759  ex-sategoelelomsuc  32786  ex-sategoelel12  32787  dfrdg2  33153  sltval2  33276  nosgnn0  33278  sltintdifex  33281  sltres  33282  sltsolem1  33293  nolt02o  33312  dfrdg4  33525  bj-1nel0  34390  bj-pr21val  34449  finxpreclem2  34807  epnsymrel  35958  sn-inelr  39590  0dioph  39719  clsk1indlem1  40748  dirkercncflem2  42746  fourierdlem60  42808  fourierdlem61  42809  afv20defat  43788  fun2dmnopgexmpl  43840  itcoval1  45077  line2ylem  45165