Theorem neii 2366

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

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

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 2365

This theorem is referenced by:  2dom  6859  updjudhcoinrg  7140  omp1eomlem  7153  nninfisol  7192  exmidomni  7201  mkvprop  7217  nninfwlporlemd  7231  nninfwlpoimlemginf  7235  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  ine0  8413  inelr  8603  xrltnr  9845  pnfnlt  9853  xrlttri3  9863  nltpnft  9880  xrpnfdc  9908  xrmnfdc  9909  xleaddadd  9953  zfz1iso  10912  3lcm2e6woprm  12224  6lcm4e12  12225  m1dvdsndvds  12386  unct  12599  fnpr2ob  12923  fvprif  12926  bj-charfunbi  15303  pwle2  15489  subctctexmid  15491  pw1nct  15493  peano3nninf  15497  nninfsellemqall  15505  nninffeq  15510