Theorem neii 2336

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

Syntax hints:   -. wn 3   = wceq 1342   =/= wne 2334

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 2335

This theorem is referenced by:  2dom  6762  updjudhcoinrg  7037  omp1eomlem  7050  nninfisol  7088  exmidomni  7097  mkvprop  7113  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  ine0  8283  inelr  8473  xrltnr  9706  pnfnlt  9714  xrlttri3  9724  nltpnft  9741  xrpnfdc  9769  xrmnfdc  9770  xleaddadd  9814  zfz1iso  10740  3lcm2e6woprm  11997  6lcm4e12  11998  m1dvdsndvds  12157  unct  12312  bj-charfunbi  13528  pwle2  13712  subctctexmid  13715  pw1nct  13717  peano3nninf  13721  nninfsellemqall  13729  nninffeq  13734