Theorem neii 2404

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

Syntax hints:   -. wn 3   = wceq 1397   =/= wne 2402

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 2403

This theorem is referenced by:  2dom  6980  updjudhcoinrg  7280  omp1eomlem  7293  nninfisol  7332  exmidomni  7341  mkvprop  7357  nninfwlporlemd  7371  nninfwlpoimlemginf  7375  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  ine0  8573  inelr  8764  xrltnr  10014  pnfnlt  10022  xrlttri3  10032  nltpnft  10049  xrpnfdc  10077  xrmnfdc  10078  xleaddadd  10122  zfz1iso  11106  hashtpglem  11111  3lcm2e6woprm  12676  6lcm4e12  12677  m1dvdsndvds  12839  unct  13081  fnpr2ob  13441  fvprif  13444  2lgslem3  15849  2lgslem4  15851  bj-charfunbi  16457  pwle2  16650  subctctexmid  16652  pw1nct  16655  peano3nninf  16660  nninfsellemqall  16668  nninffeq  16673