Theorem neii 2359

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

Syntax hints:  ¬ wn 3   = wceq 1363   ≠ wne 2357

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 2358

This theorem is referenced by:  2dom  6818  updjudhcoinrg  7093  omp1eomlem  7106  nninfisol  7144  exmidomni  7153  mkvprop  7169  nninfwlporlemd  7183  nninfwlpoimlemginf  7187  exmidfodomrlemr  7214  exmidfodomrlemrALT  7215  exmidaclem  7220  ine0  8364  inelr  8554  xrltnr  9792  pnfnlt  9800  xrlttri3  9810  nltpnft  9827  xrpnfdc  9855  xrmnfdc  9856  xleaddadd  9900  zfz1iso  10834  3lcm2e6woprm  12099  6lcm4e12  12100  m1dvdsndvds  12261  unct  12456  fnpr2ob  12777  fvprif  12780  bj-charfunbi  14834  pwle2  15020  subctctexmid  15022  pw1nct  15024  peano3nninf  15028  nninfsellemqall  15036  nninffeq  15041