Theorem neii 2405

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

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

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 2404

This theorem is referenced by:  2dom  7023  updjudhcoinrg  7323  omp1eomlem  7336  nninfisol  7375  exmidomni  7384  mkvprop  7400  nninfwlporlemd  7414  nninfwlpoimlemginf  7418  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  ine0  8616  inelr  8807  xrltnr  10057  pnfnlt  10065  xrlttri3  10075  nltpnft  10092  xrpnfdc  10120  xrmnfdc  10121  xleaddadd  10165  zfz1iso  11149  hashtpglem  11154  3lcm2e6woprm  12719  6lcm4e12  12720  m1dvdsndvds  12882  unct  13124  fnpr2ob  13484  fvprif  13487  2lgslem3  15900  2lgslem4  15902  bj-charfunbi  16507  pwle2  16700  subctctexmid  16702  pw1nct  16705  peano3nninf  16713  nninfsellemqall  16721  nninffeq  16726