Theorem neii 2416

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

Syntax hints:  ¬ wn 3   = wceq 1398   ≠ wne 2414

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 2415

This theorem is referenced by:  2dom  7059  updjudhcoinrg  7385  omp1eomlem  7398  nninfisol  7437  exmidomni  7446  mkvprop  7462  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  ine0  8684  inelr  8875  xrltnr  10131  pnfnlt  10139  xrlttri3  10149  nltpnft  10166  xrpnfdc  10194  xrmnfdc  10195  xleaddadd  10239  zfz1iso  11238  hashtpglem  11243  3lcm2e6woprm  12808  6lcm4e12  12809  m1dvdsndvds  12971  ballotfilemii  13190  unct  13277  fnpr2ob  13637  fvprif  13640  2lgslem3  16086  2lgslem4  16088  bj-charfunbi  16693  pwle2  16884  subctctexmid  16886  pw1nct  16889  peano3nninf  16897  nninfsellemqall  16905  nninffeq  16910