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  8722  inelr  8914  xrltnr  10191  pnfnlt  10199  xrlttri3  10209  nltpnft  10226  xrpnfdc  10254  xrmnfdc  10255  xleaddadd  10299  zfz1iso  11307  hashtpglem  11312  3lcm2e6woprm  12880  6lcm4e12  12881  m1dvdsndvds  13047  ballotfilemii  13295  unct  13382  fnpr2ob  13710  fvprif  13713  2lgslem3  16318  2lgslem4  16320  bj-charfunbi  16935  pwle2  17126  subctctexmid  17128  pw1nct  17131  peano3nninf  17148  nninfsellemqall  17156  nninffeq  17161