Theorem neii 2308

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

Syntax hints:   -. wn 3   = wceq 1331   =/= wne 2306

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

This theorem depends on definitions:  df-bi 116  df-ne 2307

This theorem is referenced by:  2dom  6692  updjudhcoinrg  6959  omp1eomlem  6972  exmidomni  7007  mkvprop  7025  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  ine0  8149  inelr  8339  xrltnr  9559  pnfnlt  9566  xrlttri3  9576  nltpnft  9590  xrpnfdc  9618  xrmnfdc  9619  xleaddadd  9663  zfz1iso  10577  3lcm2e6woprm  11756  6lcm4e12  11757  unct  11943  pwle2  13182  subctctexmid  13185  peano3nninf  13190  nninfsellemqall  13200  nninffeq  13205