Theorem neii 2945

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

Syntax hints:  ¬ wn 3   = wceq 1631   ≠ wne 2943

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 197  df-ne 2944

This theorem is referenced by:  nesymi  3000  nemtbir  3038  snsssn  4505  2dom  8182  map2xp  8286  updjudhcoinrg  8959  pm54.43lem  9025  canthp1lem2  9677  ine0  10667  inelr  11212  xrltnr  12158  pnfnlt  12167  prprrab  13457  wrdlen2i  13896  3lcm2e6woprm  15536  6lcm4e12  15537  m1dvdsndvds  15710  xpsfrnel2  16433  pmatcollpw3fi1lem1  20811  sinhalfpilem  24436  coseq1  24495  2lgslem3  25350  2lgslem4  25352  axlowdimlem13  26055  axlowdim1  26060  umgredgnlp  26264  wwlksnext  27037  norm1exi  28447  largei  29466  ind1a  30421  ballotlemii  30905  sgnnbi  30947  sgnpbi  30948  dfrdg2  32037  sltval2  32146  nosgnn0  32148  sltintdifex  32151  sltres  32152  sltsolem1  32163  nolt02o  32182  dfrdg4  32395  bj-1nel0  33272  bj-pr21val  33332  finxpreclem2  33564  epnsymrel  34650  0dioph  37868  clsk1indlem1  38869  dirkercncflem2  40838  fourierdlem60  40900  fourierdlem61  40901  fun2dmnopgexmpl  41826