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  6966  updjudhcoinrg  7256  omp1eomlem  7269  nninfisol  7308  exmidomni  7317  mkvprop  7333  nninfwlporlemd  7347  nninfwlpoimlemginf  7351  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidaclem  7398  ine0  8548  inelr  8739  xrltnr  9983  pnfnlt  9991  xrlttri3  10001  nltpnft  10018  xrpnfdc  10046  xrmnfdc  10047  xleaddadd  10091  zfz1iso  11071  3lcm2e6woprm  12616  6lcm4e12  12617  m1dvdsndvds  12779  unct  13021  fnpr2ob  13381  fvprif  13384  2lgslem3  15788  2lgslem4  15790  bj-charfunbi  16198  pwle2  16393  subctctexmid  16395  pw1nct  16398  peano3nninf  16403  nninfsellemqall  16411  nninffeq  16416