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  6804  updjudhcoinrg  7079  omp1eomlem  7092  nninfisol  7130  exmidomni  7139  mkvprop  7155  nninfwlporlemd  7169  nninfwlpoimlemginf  7173  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  ine0  8350  inelr  8540  xrltnr  9778  pnfnlt  9786  xrlttri3  9796  nltpnft  9813  xrpnfdc  9841  xrmnfdc  9842  xleaddadd  9886  zfz1iso  10820  3lcm2e6woprm  12085  6lcm4e12  12086  m1dvdsndvds  12247  unct  12442  fnpr2ob  12758  fvprif  12761  bj-charfunbi  14533  pwle2  14718  subctctexmid  14720  pw1nct  14722  peano3nninf  14726  nninfsellemqall  14734  nninffeq  14739