Theorem neii 2369

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

Syntax hints:  ¬ wn 3   = wceq 1364   ≠ wne 2367

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 2368

This theorem is referenced by:  2dom  6873  updjudhcoinrg  7156  omp1eomlem  7169  nninfisol  7208  exmidomni  7217  mkvprop  7233  nninfwlporlemd  7247  nninfwlpoimlemginf  7251  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  ine0  8439  inelr  8630  xrltnr  9873  pnfnlt  9881  xrlttri3  9891  nltpnft  9908  xrpnfdc  9936  xrmnfdc  9937  xleaddadd  9981  zfz1iso  10952  3lcm2e6woprm  12281  6lcm4e12  12282  m1dvdsndvds  12444  unct  12686  fnpr2ob  13044  fvprif  13047  2lgslem3  15450  2lgslem4  15452  bj-charfunbi  15565  pwle2  15753  subctctexmid  15755  pw1nct  15758  peano3nninf  15762  nninfsellemqall  15770  nninffeq  15775