Theorem neii 2422

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  2dom  7099  updjudhcoinrg  7428  omp1eomlem  7441  nninfisol  7480  exmidomni  7489  mkvprop  7505  nninfwlporlemd  7519  nninfwlpoimlemginf  7523  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  ine0  8729  inelr  8921  xrltnr  10198  pnfnlt  10206  xrlttri3  10216  nltpnft  10233  xrpnfdc  10261  xrmnfdc  10262  xleaddadd  10306  zfz1iso  11315  hashtpglem  11320  3lcm2e6woprm  12889  6lcm4e12  12890  m1dvdsndvds  13056  ballotfilemii  13304  unct  13391  fnpr2ob  13720  fvprif  13723  2lgslem3  16458  2lgslem4  16460  bj-charfunbi  17075  pwle2  17266  subctctexmid  17268  pw1nct  17271  idjudju  17285  peano3nninf  17289  nninfsellemqall  17297  nninffeq  17302