Theorem neii 2404

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

Syntax hints:  ¬ wn 3   = wceq 1397   ≠ wne 2402

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 2403

This theorem is referenced by:  2dom  6980  updjudhcoinrg  7280  omp1eomlem  7293  nninfisol  7332  exmidomni  7341  mkvprop  7357  nninfwlporlemd  7371  nninfwlpoimlemginf  7375  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  ine0  8573  inelr  8764  xrltnr  10014  pnfnlt  10022  xrlttri3  10032  nltpnft  10049  xrpnfdc  10077  xrmnfdc  10078  xleaddadd  10122  zfz1iso  11106  hashtpglem  11111  3lcm2e6woprm  12663  6lcm4e12  12664  m1dvdsndvds  12826  unct  13068  fnpr2ob  13428  fvprif  13431  2lgslem3  15836  2lgslem4  15838  bj-charfunbi  16432  pwle2  16625  subctctexmid  16627  pw1nct  16630  peano3nninf  16635  nninfsellemqall  16643  nninffeq  16648