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 ⊢ ¬ 𝐴 = 𝐵

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  7087  updjudhcoinrg  7415  omp1eomlem  7428  nninfisol  7467  exmidomni  7476  mkvprop  7492  nninfwlporlemd  7506  nninfwlpoimlemginf  7510  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  ine0  8715  inelr  8906  xrltnr  10164  pnfnlt  10172  xrlttri3  10182  nltpnft  10199  xrpnfdc  10227  xrmnfdc  10228  xleaddadd  10272  zfz1iso  11276  hashtpglem  11281  3lcm2e6woprm  12847  6lcm4e12  12848  m1dvdsndvds  13010  ballotfilemii  13229  unct  13316  fnpr2ob  13644  fvprif  13647  2lgslem3  16203  2lgslem4  16205  bj-charfunbi  16820  pwle2  17011  subctctexmid  17013  pw1nct  17016  peano3nninf  17024  nninfsellemqall  17032  nninffeq  17037