Theorem neii 2416

Description: Inference associated with df-ne 2415. (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 2415	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 145	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = wceq 1398   ≠ wne 2414

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 2415

This theorem is referenced by:  2dom  7059  updjudhcoinrg  7385  omp1eomlem  7398  nninfisol  7437  exmidomni  7446  mkvprop  7462  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  ine0  8685  inelr  8876  xrltnr  10134  pnfnlt  10142  xrlttri3  10152  nltpnft  10169  xrpnfdc  10197  xrmnfdc  10198  xleaddadd  10242  zfz1iso  11241  hashtpglem  11246  3lcm2e6woprm  12812  6lcm4e12  12813  m1dvdsndvds  12975  ballotfilemii  13194  unct  13281  fnpr2ob  13608  fvprif  13611  2lgslem3  16104  2lgslem4  16106  bj-charfunbi  16721  pwle2  16912  subctctexmid  16914  pw1nct  16917  peano3nninf  16925  nninfsellemqall  16933  nninffeq  16938