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  7422  omp1eomlem  7435  nninfisol  7474  exmidomni  7483  mkvprop  7499  nninfwlporlemd  7513  nninfwlpoimlemginf  7517  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  ine0  8723  inelr  8915  xrltnr  10192  pnfnlt  10200  xrlttri3  10210  nltpnft  10227  xrpnfdc  10255  xrmnfdc  10256  xleaddadd  10300  zfz1iso  11309  hashtpglem  11314  3lcm2e6woprm  12883  6lcm4e12  12884  m1dvdsndvds  13050  ballotfilemii  13298  unct  13385  fnpr2ob  13714  fvprif  13717  2lgslem3  16386  2lgslem4  16388  bj-charfunbi  17003  pwle2  17194  subctctexmid  17196  pw1nct  17199  peano3nninf  17216  nninfsellemqall  17224  nninffeq  17229