Theorem neii 2422

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

This proof depends on syntax axioms:   -. wn 3   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  2dom  7093  updjudhcoinrg  7421  omp1eomlem  7434  nninfisol  7473  exmidomni  7482  mkvprop  7498  nninfwlporlemd  7512  nninfwlpoimlemginf  7516  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  ine0  8721  inelr  8912  xrltnr  10181  pnfnlt  10189  xrlttri3  10199  nltpnft  10216  xrpnfdc  10244  xrmnfdc  10245  xleaddadd  10289  zfz1iso  11293  hashtpglem  11298  3lcm2e6woprm  12864  6lcm4e12  12865  m1dvdsndvds  13027  ballotfilemii  13246  unct  13333  fnpr2ob  13661  fvprif  13664  2lgslem3  16220  2lgslem4  16222  bj-charfunbi  16837  pwle2  17028  subctctexmid  17030  pw1nct  17033  peano3nninf  17050  nninfsellemqall  17058  nninffeq  17063