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  6958  updjudhcoinrg  7248  omp1eomlem  7261  nninfisol  7300  exmidomni  7309  mkvprop  7325  nninfwlporlemd  7339  nninfwlpoimlemginf  7343  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  ine0  8540  inelr  8731  xrltnr  9975  pnfnlt  9983  xrlttri3  9993  nltpnft  10010  xrpnfdc  10038  xrmnfdc  10039  xleaddadd  10083  zfz1iso  11063  3lcm2e6woprm  12608  6lcm4e12  12609  m1dvdsndvds  12771  unct  13013  fnpr2ob  13373  fvprif  13376  2lgslem3  15780  2lgslem4  15782  bj-charfunbi  16174  pwle2  16364  subctctexmid  16366  pw1nct  16369  peano3nninf  16373  nninfsellemqall  16381  nninffeq  16386