Theorem neii 2402

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

Syntax hints:  ¬ wn 3   = wceq 1395   ≠ wne 2400

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 2401

This theorem is referenced by:  2dom  6971  updjudhcoinrg  7264  omp1eomlem  7277  nninfisol  7316  exmidomni  7325  mkvprop  7341  nninfwlporlemd  7355  nninfwlpoimlemginf  7359  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  ine0  8556  inelr  8747  xrltnr  9992  pnfnlt  10000  xrlttri3  10010  nltpnft  10027  xrpnfdc  10055  xrmnfdc  10056  xleaddadd  10100  zfz1iso  11081  3lcm2e6woprm  12629  6lcm4e12  12630  m1dvdsndvds  12792  unct  13034  fnpr2ob  13394  fvprif  13397  2lgslem3  15801  2lgslem4  15803  bj-charfunbi  16283  pwle2  16477  subctctexmid  16479  pw1nct  16482  peano3nninf  16487  nninfsellemqall  16495  nninffeq  16500