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

Syntax hints:   -. wn 3   = wceq 1402   =/= wne 2420

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 2421

This theorem is referenced by:  2dom  7083  updjudhcoinrg  7411  omp1eomlem  7424  nninfisol  7463  exmidomni  7472  mkvprop  7488  nninfwlporlemd  7502  nninfwlpoimlemginf  7506  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  ine0  8711  inelr  8902  xrltnr  10160  pnfnlt  10168  xrlttri3  10178  nltpnft  10195  xrpnfdc  10223  xrmnfdc  10224  xleaddadd  10268  zfz1iso  11271  hashtpglem  11276  3lcm2e6woprm  12842  6lcm4e12  12843  m1dvdsndvds  13005  ballotfilemii  13224  unct  13311  fnpr2ob  13638  fvprif  13641  2lgslem3  16134  2lgslem4  16136  bj-charfunbi  16751  pwle2  16942  subctctexmid  16944  pw1nct  16947  peano3nninf  16955  nninfsellemqall  16963  nninffeq  16968