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  6956  updjudhcoinrg  7244  omp1eomlem  7257  nninfisol  7296  exmidomni  7305  mkvprop  7321  nninfwlporlemd  7335  nninfwlpoimlemginf  7339  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  ine0  8536  inelr  8727  xrltnr  9971  pnfnlt  9979  xrlttri3  9989  nltpnft  10006  xrpnfdc  10034  xrmnfdc  10035  xleaddadd  10079  zfz1iso  11058  3lcm2e6woprm  12603  6lcm4e12  12604  m1dvdsndvds  12766  unct  13008  fnpr2ob  13368  fvprif  13371  2lgslem3  15774  2lgslem4  15776  bj-charfunbi  16132  pwle2  16323  subctctexmid  16325  pw1nct  16328  peano3nninf  16332  nninfsellemqall  16340  nninffeq  16345