Theorem neii 2796

Description: Inference associated with df-ne 2795. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neii.1	|- A =/= B

Assertion

Ref	Expression
neii	|- -. A = B

Proof of Theorem neii

Step	Hyp	Ref	Expression
1		neii.1	. 2 |- A =/= B
2		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	mpbi 220	1 |- -. A = B

Syntax hints:   -. wn 3   = wceq 1483   =/= wne 2794

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 2795

This theorem is referenced by:  nesymi  2851  nemtbir  2889  snsssn  4372  2dom  8029  map2xp  8130  pm54.43lem  8825  canthp1lem2  9475  ine0  10465  inelr  11010  xrltnr  11953  pnfnlt  11962  prprrab  13255  wrdlen2i  13686  3lcm2e6woprm  15328  6lcm4e12  15329  m1dvdsndvds  15503  xpsfrnel2  16225  pmatcollpw3fi1lem1  20591  sinhalfpilem  24215  coseq1  24274  2lgslem3  25129  2lgslem4  25131  axlowdimlem13  25834  axlowdim1  25839  umgredgnlp  26042  uvtxa01vtx  26298  wwlksnext  26788  norm1exi  28107  largei  29126  ind1a  30081  ballotlemii  30565  sgnnbi  30607  sgnpbi  30608  dfrdg2  31701  sltval2  31809  nosgnn0  31811  sltintdifex  31814  sltres  31815  sltsolem1  31826  nolt02o  31845  dfrdg4  32058  bj-1nel0  32941  bj-pr21val  33001  finxpreclem2  33227  0dioph  37342  clsk1indlem1  38343  dirkercncflem2  40321  fourierdlem60  40383  fourierdlem61  40384  fun2dmnopgexmpl  41303