Theorem neii 2416

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

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

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 2415

This theorem is referenced by:  2dom  7059  updjudhcoinrg  7385  omp1eomlem  7398  nninfisol  7437  exmidomni  7446  mkvprop  7462  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  ine0  8684  inelr  8875  xrltnr  10131  pnfnlt  10139  xrlttri3  10149  nltpnft  10166  xrpnfdc  10194  xrmnfdc  10195  xleaddadd  10239  zfz1iso  11238  hashtpglem  11243  3lcm2e6woprm  12808  6lcm4e12  12809  m1dvdsndvds  12971  ballotfilemii  13190  unct  13277  fnpr2ob  13604  fvprif  13607  2lgslem3  16100  2lgslem4  16102  bj-charfunbi  16707  pwle2  16898  subctctexmid  16900  pw1nct  16903  peano3nninf  16911  nninfsellemqall  16919  nninffeq  16924