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  7099  updjudhcoinrg  7427  omp1eomlem  7440  nninfisol  7479  exmidomni  7488  mkvprop  7504  nninfwlporlemd  7518  nninfwlpoimlemginf  7522  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  ine0  8728  inelr  8920  xrltnr  10197  pnfnlt  10205  xrlttri3  10215  nltpnft  10232  xrpnfdc  10260  xrmnfdc  10261  xleaddadd  10305  zfz1iso  11314  hashtpglem  11319  3lcm2e6woprm  12888  6lcm4e12  12889  m1dvdsndvds  13055  ballotfilemii  13303  unct  13390  fnpr2ob  13719  fvprif  13722  2lgslem3  16442  2lgslem4  16444  bj-charfunbi  17059  pwle2  17250  subctctexmid  17252  pw1nct  17255  idjudju  17269  peano3nninf  17273  nninfsellemqall  17281  nninffeq  17286