Theorem neii 2378

Description: Inference associated with df-ne 2377. (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 2377	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	mpbi 145	1 |- -. A = B

Syntax hints:   -. wn 3   = wceq 1373   =/= wne 2376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-ne 2377

This theorem is referenced by:  2dom  6897  updjudhcoinrg  7183  omp1eomlem  7196  nninfisol  7235  exmidomni  7244  mkvprop  7260  nninfwlporlemd  7274  nninfwlpoimlemginf  7278  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  ine0  8466  inelr  8657  xrltnr  9901  pnfnlt  9909  xrlttri3  9919  nltpnft  9936  xrpnfdc  9964  xrmnfdc  9965  xleaddadd  10009  zfz1iso  10986  3lcm2e6woprm  12408  6lcm4e12  12409  m1dvdsndvds  12571  unct  12813  fnpr2ob  13172  fvprif  13175  2lgslem3  15578  2lgslem4  15580  bj-charfunbi  15747  pwle2  15935  subctctexmid  15937  pw1nct  15940  peano3nninf  15944  nninfsellemqall  15952  nninffeq  15957