Theorem neii 2342

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

Syntax hints:  ¬ wn 3   = wceq 1348   ≠ wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-ne 2341

This theorem is referenced by:  2dom  6783  updjudhcoinrg  7058  omp1eomlem  7071  nninfisol  7109  exmidomni  7118  mkvprop  7134  nninfwlporlemd  7148  nninfwlpoimlemginf  7152  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  ine0  8313  inelr  8503  xrltnr  9736  pnfnlt  9744  xrlttri3  9754  nltpnft  9771  xrpnfdc  9799  xrmnfdc  9800  xleaddadd  9844  zfz1iso  10776  3lcm2e6woprm  12040  6lcm4e12  12041  m1dvdsndvds  12202  unct  12397  bj-charfunbi  13846  pwle2  14031  subctctexmid  14034  pw1nct  14036  peano3nninf  14040  nninfsellemqall  14048  nninffeq  14053