Theorem neii 2349

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

Syntax hints:  ¬ wn 3   = wceq 1353   ≠ wne 2347

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 2348

This theorem is referenced by:  2dom  6805  updjudhcoinrg  7080  omp1eomlem  7093  nninfisol  7131  exmidomni  7140  mkvprop  7156  nninfwlporlemd  7170  nninfwlpoimlemginf  7174  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  ine0  8351  inelr  8541  xrltnr  9779  pnfnlt  9787  xrlttri3  9797  nltpnft  9814  xrpnfdc  9842  xrmnfdc  9843  xleaddadd  9887  zfz1iso  10821  3lcm2e6woprm  12086  6lcm4e12  12087  m1dvdsndvds  12248  unct  12443  fnpr2ob  12759  fvprif  12762  bj-charfunbi  14566  pwle2  14751  subctctexmid  14753  pw1nct  14755  peano3nninf  14759  nninfsellemqall  14767  nninffeq  14772