Theorem neii 2326

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

Syntax hints:  ¬ wn 3   = wceq 1332   ≠ wne 2324

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 2325

This theorem is referenced by:  2dom  6739  updjudhcoinrg  7011  omp1eomlem  7024  exmidomni  7064  mkvprop  7080  exmidfodomrlemr  7116  exmidfodomrlemrALT  7117  exmidaclem  7122  ine0  8248  inelr  8438  xrltnr  9664  pnfnlt  9672  xrlttri3  9682  nltpnft  9696  xrpnfdc  9724  xrmnfdc  9725  xleaddadd  9769  zfz1iso  10689  3lcm2e6woprm  11934  6lcm4e12  11935  unct  12122  bj-charfunbi  13324  pwle2  13509  subctctexmid  13512  pw1nct  13514  peano3nninf  13519  nninfsellemqall  13528  nninffeq  13533