Theorem neii 2257

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

Syntax hints:  ¬ wn 3   = wceq 1289   ≠ wne 2255

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

This theorem depends on definitions:  df-bi 115  df-ne 2256

This theorem is referenced by:  2dom  6502  updjudhcoinrg  6751  exmidomni  6777  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  ine0  7851  inelr  8037  xrltnr  9219  pnfnlt  9226  xrlttri3  9236  nltpnft  9248  zfz1iso  10211  3lcm2e6woprm  11161  6lcm4e12  11162  peano3nninf  11554  nninfsellemqall  11564