Theorem neii 2402

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

Syntax hints:   -. wn 3   = wceq 1395   =/= wne 2400

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 2401

This theorem is referenced by:  2dom  6966  updjudhcoinrg  7259  omp1eomlem  7272  nninfisol  7311  exmidomni  7320  mkvprop  7336  nninfwlporlemd  7350  nninfwlpoimlemginf  7354  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  ine0  8551  inelr  8742  xrltnr  9987  pnfnlt  9995  xrlttri3  10005  nltpnft  10022  xrpnfdc  10050  xrmnfdc  10051  xleaddadd  10095  zfz1iso  11076  3lcm2e6woprm  12623  6lcm4e12  12624  m1dvdsndvds  12786  unct  13028  fnpr2ob  13388  fvprif  13391  2lgslem3  15795  2lgslem4  15797  bj-charfunbi  16233  pwle2  16427  subctctexmid  16429  pw1nct  16432  peano3nninf  16437  nninfsellemqall  16445  nninffeq  16450