Theorem neii 2422

Description: Inference associated with df-ne 2421. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neii.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
neii	⊢ ¬ 𝐴 = 𝐵

Proof of Theorem neii

Step	Hyp	Ref	Expression
1		neii.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		df-ne 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐴 = 𝐵

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  11308  hashtpglem  11313  3lcm2e6woprm  12882  6lcm4e12  12883  m1dvdsndvds  13049  ballotfilemii  13297  unct  13384  fnpr2ob  13712  fvprif  13715  2lgslem3  16342  2lgslem4  16344  bj-charfunbi  16959  pwle2  17150  subctctexmid  17152  pw1nct  17155  peano3nninf  17172  nninfsellemqall  17180  nninffeq  17185