Theorem neii 2380

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

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

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 2379

This theorem is referenced by:  2dom  6921  updjudhcoinrg  7209  omp1eomlem  7222  nninfisol  7261  exmidomni  7270  mkvprop  7286  nninfwlporlemd  7300  nninfwlpoimlemginf  7304  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  ine0  8501  inelr  8692  xrltnr  9936  pnfnlt  9944  xrlttri3  9954  nltpnft  9971  xrpnfdc  9999  xrmnfdc  10000  xleaddadd  10044  zfz1iso  11023  3lcm2e6woprm  12523  6lcm4e12  12524  m1dvdsndvds  12686  unct  12928  fnpr2ob  13287  fvprif  13290  2lgslem3  15693  2lgslem4  15695  bj-charfunbi  15946  pwle2  16137  subctctexmid  16139  pw1nct  16142  peano3nninf  16146  nninfsellemqall  16154  nninffeq  16159