Theorem neii 2311

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

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

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 2310

This theorem is referenced by:  2dom  6707  updjudhcoinrg  6974  omp1eomlem  6987  exmidomni  7022  mkvprop  7040  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  ine0  8180  inelr  8370  xrltnr  9596  pnfnlt  9603  xrlttri3  9613  nltpnft  9627  xrpnfdc  9655  xrmnfdc  9656  xleaddadd  9700  zfz1iso  10616  3lcm2e6woprm  11803  6lcm4e12  11804  unct  11991  pwle2  13366  subctctexmid  13369  pw1nct  13371  peano3nninf  13376  nninfsellemqall  13386  nninffeq  13391