Theorem neii 2349

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

Syntax hints:   -. wn 3   = wceq 1353   =/= wne 2347

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 2348

This theorem is referenced by:  2dom  6807  updjudhcoinrg  7082  omp1eomlem  7095  nninfisol  7133  exmidomni  7142  mkvprop  7158  nninfwlporlemd  7172  nninfwlpoimlemginf  7176  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  ine0  8353  inelr  8543  xrltnr  9781  pnfnlt  9789  xrlttri3  9799  nltpnft  9816  xrpnfdc  9844  xrmnfdc  9845  xleaddadd  9889  zfz1iso  10823  3lcm2e6woprm  12088  6lcm4e12  12089  m1dvdsndvds  12250  unct  12445  fnpr2ob  12764  fvprif  12767  bj-charfunbi  14602  pwle2  14787  subctctexmid  14789  pw1nct  14791  peano3nninf  14795  nninfsellemqall  14803  nninffeq  14808