Theorem neii 2973

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

Syntax hints:  ¬ wn 3   = wceq 1653   ≠ wne 2971

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 199  df-ne 2972

This theorem is referenced by:  nesymi  3028  nemtbir  3066  snsssn  4558  2dom  8268  map2xp  8372  updjudhcoinrg  9045  pm54.43lem  9111  canthp1lem2  9763  ine0  10757  inelr  11302  xrltnr  12200  pnfnlt  12209  prprrab  13504  wrdlen2i  14027  3lcm2e6woprm  15663  6lcm4e12  15664  m1dvdsndvds  15836  xpsfrnel2  16540  pmatcollpw3fi1lem1  20919  sinhalfpilem  24557  coseq1  24616  2lgslem3  25481  2lgslem4  25483  axlowdimlem13  26191  axlowdim1  26196  umgredgnlp  26383  wwlksnext  27162  norm1exi  28632  largei  29651  ind1a  30597  ballotlemii  31082  sgnnbi  31124  sgnpbi  31125  dfrdg2  32213  sltval2  32322  nosgnn0  32324  sltintdifex  32327  sltres  32328  sltsolem1  32339  nolt02o  32358  dfrdg4  32571  bj-1nel0  33433  bj-pr21val  33493  finxpreclem2  33725  epnsymrel  34802  0dioph  38128  clsk1indlem1  39125  dirkercncflem2  41064  fourierdlem60  41126  fourierdlem61  41127  afv20defat  42086  fun2dmnopgexmpl  42139