Theorem neii 2338

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

Syntax hints:   -. wn 3   = wceq 1343   =/= wne 2336

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 2337

This theorem is referenced by:  2dom  6771  updjudhcoinrg  7046  omp1eomlem  7059  nninfisol  7097  exmidomni  7106  mkvprop  7122  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  ine0  8292  inelr  8482  xrltnr  9715  pnfnlt  9723  xrlttri3  9733  nltpnft  9750  xrpnfdc  9778  xrmnfdc  9779  xleaddadd  9823  zfz1iso  10754  3lcm2e6woprm  12018  6lcm4e12  12019  m1dvdsndvds  12180  unct  12375  bj-charfunbi  13693  pwle2  13878  subctctexmid  13881  pw1nct  13883  peano3nninf  13887  nninfsellemqall  13895  nninffeq  13900