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  7093  updjudhcoinrg  7421  omp1eomlem  7434  nninfisol  7473  exmidomni  7482  mkvprop  7498  nninfwlporlemd  7512  nninfwlpoimlemginf  7516  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  ine0  8721  inelr  8913  xrltnr  10183  pnfnlt  10191  xrlttri3  10201  nltpnft  10218  xrpnfdc  10246  xrmnfdc  10247  xleaddadd  10291  zfz1iso  11295  hashtpglem  11300  3lcm2e6woprm  12866  6lcm4e12  12867  m1dvdsndvds  13029  ballotfilemii  13248  unct  13335  fnpr2ob  13663  fvprif  13666  2lgslem3  16232  2lgslem4  16234  bj-charfunbi  16849  pwle2  17040  subctctexmid  17042  pw1nct  17045  peano3nninf  17062  nninfsellemqall  17070  nninffeq  17075