Theorem neii 2362

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

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

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 2361

This theorem is referenced by:  2dom  6832  updjudhcoinrg  7111  omp1eomlem  7124  nninfisol  7162  exmidomni  7171  mkvprop  7187  nninfwlporlemd  7201  nninfwlpoimlemginf  7205  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  exmidaclem  7238  ine0  8382  inelr  8572  xrltnr  9811  pnfnlt  9819  xrlttri3  9829  nltpnft  9846  xrpnfdc  9874  xrmnfdc  9875  xleaddadd  9919  zfz1iso  10856  3lcm2e6woprm  12121  6lcm4e12  12122  m1dvdsndvds  12283  unct  12496  fnpr2ob  12819  fvprif  12822  bj-charfunbi  15041  pwle2  15227  subctctexmid  15229  pw1nct  15231  peano3nninf  15235  nninfsellemqall  15243  nninffeq  15248