Theorem neii 2414

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

Syntax hints:   -. wn 3   = wceq 1398   =/= wne 2412

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 2413

This theorem is referenced by:  2dom  7046  updjudhcoinrg  7372  omp1eomlem  7385  nninfisol  7424  exmidomni  7433  mkvprop  7449  nninfwlporlemd  7463  nninfwlpoimlemginf  7467  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  ine0  8667  inelr  8858  xrltnr  10112  pnfnlt  10120  xrlttri3  10130  nltpnft  10147  xrpnfdc  10175  xrmnfdc  10176  xleaddadd  10220  zfz1iso  11213  hashtpglem  11218  3lcm2e6woprm  12783  6lcm4e12  12784  m1dvdsndvds  12946  unct  13193  fnpr2ob  13553  fvprif  13556  2lgslem3  15974  2lgslem4  15976  bj-charfunbi  16581  pwle2  16772  subctctexmid  16774  pw1nct  16777  peano3nninf  16785  nninfsellemqall  16793  nninffeq  16798