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  6979  updjudhcoinrg  7279  omp1eomlem  7292  nninfisol  7331  exmidomni  7340  mkvprop  7356  nninfwlporlemd  7370  nninfwlpoimlemginf  7374  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  ine0  8572  inelr  8763  xrltnr  10013  pnfnlt  10021  xrlttri3  10031  nltpnft  10048  xrpnfdc  10076  xrmnfdc  10077  xleaddadd  10121  zfz1iso  11104  3lcm2e6woprm  12657  6lcm4e12  12658  m1dvdsndvds  12820  unct  13062  fnpr2ob  13422  fvprif  13425  2lgslem3  15829  2lgslem4  15831  bj-charfunbi  16406  pwle2  16599  subctctexmid  16601  pw1nct  16604  peano3nninf  16609  nninfsellemqall  16617  nninffeq  16622