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  6975  updjudhcoinrg  7271  omp1eomlem  7284  nninfisol  7323  exmidomni  7332  mkvprop  7348  nninfwlporlemd  7362  nninfwlpoimlemginf  7366  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  ine0  8563  inelr  8754  xrltnr  10004  pnfnlt  10012  xrlttri3  10022  nltpnft  10039  xrpnfdc  10067  xrmnfdc  10068  xleaddadd  10112  zfz1iso  11095  3lcm2e6woprm  12648  6lcm4e12  12649  m1dvdsndvds  12811  unct  13053  fnpr2ob  13413  fvprif  13416  2lgslem3  15820  2lgslem4  15822  bj-charfunbi  16342  pwle2  16535  subctctexmid  16537  pw1nct  16540  peano3nninf  16545  nninfsellemqall  16553  nninffeq  16558