Theorem neii 2369

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

Syntax hints:   -. wn 3   = wceq 1364   =/= wne 2367

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 2368

This theorem is referenced by:  2dom  6873  updjudhcoinrg  7156  omp1eomlem  7169  nninfisol  7208  exmidomni  7217  mkvprop  7233  nninfwlporlemd  7247  nninfwlpoimlemginf  7251  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  ine0  8437  inelr  8628  xrltnr  9871  pnfnlt  9879  xrlttri3  9889  nltpnft  9906  xrpnfdc  9934  xrmnfdc  9935  xleaddadd  9979  zfz1iso  10950  3lcm2e6woprm  12279  6lcm4e12  12280  m1dvdsndvds  12442  unct  12684  fnpr2ob  13042  fvprif  13045  2lgslem3  15426  2lgslem4  15428  bj-charfunbi  15541  pwle2  15729  subctctexmid  15731  pw1nct  15734  peano3nninf  15738  nninfsellemqall  15746  nninffeq  15751