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  7098  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  10199  pnfnlt  10207  xrlttri3  10217  nltpnft  10234  xrpnfdc  10262  xrmnfdc  10263  xleaddadd  10307  zfz1iso  11316  hashtpglem  11321  3lcm2e6woprm  12890  6lcm4e12  12891  m1dvdsndvds  13057  ballotfilemii  13305  unct  13392  fnpr2ob  13721  fvprif  13724  2lgslem3  16437  2lgslem4  16439  bj-charfunbi  17054  pwle2  17245  subctctexmid  17247  pw1nct  17250  idjudju  17264  peano3nninf  17268  nninfsellemqall  17276  nninffeq  17281