Theorem neii 2414

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

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

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 2413

This theorem is referenced by:  2dom  7045  updjudhcoinrg  7371  omp1eomlem  7384  nninfisol  7423  exmidomni  7432  mkvprop  7448  nninfwlporlemd  7462  nninfwlpoimlemginf  7466  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidaclem  7514  ine0  8666  inelr  8857  xrltnr  10111  pnfnlt  10119  xrlttri3  10129  nltpnft  10146  xrpnfdc  10174  xrmnfdc  10175  xleaddadd  10219  zfz1iso  11209  hashtpglem  11214  3lcm2e6woprm  12779  6lcm4e12  12780  m1dvdsndvds  12942  unct  13185  fnpr2ob  13545  fvprif  13548  2lgslem3  15966  2lgslem4  15968  bj-charfunbi  16573  pwle2  16764  subctctexmid  16766  pw1nct  16769  peano3nninf  16777  nninfsellemqall  16785  nninffeq  16790