Theorem neii 2310

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

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

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 2309

This theorem is referenced by:  2dom  6699  updjudhcoinrg  6966  omp1eomlem  6979  exmidomni  7014  mkvprop  7032  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  ine0  8156  inelr  8346  xrltnr  9566  pnfnlt  9573  xrlttri3  9583  nltpnft  9597  xrpnfdc  9625  xrmnfdc  9626  xleaddadd  9670  zfz1iso  10584  3lcm2e6woprm  11767  6lcm4e12  11768  unct  11954  pwle2  13193  subctctexmid  13196  peano3nninf  13201  nninfsellemqall  13211  nninffeq  13216