Theorem neii 2402

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

Syntax hints:  ¬ wn 3   = wceq 1395   ≠ wne 2400

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 2401

This theorem is referenced by:  2dom  6975  updjudhcoinrg  7274  omp1eomlem  7287  nninfisol  7326  exmidomni  7335  mkvprop  7351  nninfwlporlemd  7365  nninfwlpoimlemginf  7369  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidaclem  7416  ine0  8566  inelr  8757  xrltnr  10007  pnfnlt  10015  xrlttri3  10025  nltpnft  10042  xrpnfdc  10070  xrmnfdc  10071  xleaddadd  10115  zfz1iso  11098  3lcm2e6woprm  12651  6lcm4e12  12652  m1dvdsndvds  12814  unct  13056  fnpr2ob  13416  fvprif  13419  2lgslem3  15823  2lgslem4  15825  bj-charfunbi  16356  pwle2  16549  subctctexmid  16551  pw1nct  16554  peano3nninf  16559  nninfsellemqall  16567  nninffeq  16572