Theorem neii 2405

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

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

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 2404

This theorem is referenced by:  2dom  7023  updjudhcoinrg  7323  omp1eomlem  7336  nninfisol  7375  exmidomni  7384  mkvprop  7400  nninfwlporlemd  7414  nninfwlpoimlemginf  7418  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  ine0  8615  inelr  8806  xrltnr  10058  pnfnlt  10066  xrlttri3  10076  nltpnft  10093  xrpnfdc  10121  xrmnfdc  10122  xleaddadd  10166  zfz1iso  11151  hashtpglem  11156  3lcm2e6woprm  12721  6lcm4e12  12722  m1dvdsndvds  12884  unct  13126  fnpr2ob  13486  fvprif  13489  2lgslem3  15903  2lgslem4  15905  bj-charfunbi  16510  pwle2  16703  subctctexmid  16705  pw1nct  16708  peano3nninf  16716  nninfsellemqall  16724  nninffeq  16729