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  7097  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  10198  pnfnlt  10206  xrlttri3  10216  nltpnft  10233  xrpnfdc  10261  xrmnfdc  10262  xleaddadd  10306  zfz1iso  11315  hashtpglem  11320  3lcm2e6woprm  12889  6lcm4e12  12890  m1dvdsndvds  13056  ballotfilemii  13304  unct  13391  fnpr2ob  13720  fvprif  13723  2lgslem3  16425  2lgslem4  16427  bj-charfunbi  17042  pwle2  17233  subctctexmid  17235  pw1nct  17238  idjudju  17252  peano3nninf  17256  nninfsellemqall  17264  nninffeq  17269