Theorem neii 2369

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

Syntax hints:  ¬ wn 3   = wceq 1364   ≠ wne 2367

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 2368

This theorem is referenced by:  2dom  6864  updjudhcoinrg  7147  omp1eomlem  7160  nninfisol  7199  exmidomni  7208  mkvprop  7224  nninfwlporlemd  7238  nninfwlpoimlemginf  7242  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  ine0  8420  inelr  8611  xrltnr  9854  pnfnlt  9862  xrlttri3  9872  nltpnft  9889  xrpnfdc  9917  xrmnfdc  9918  xleaddadd  9962  zfz1iso  10933  3lcm2e6woprm  12254  6lcm4e12  12255  m1dvdsndvds  12417  unct  12659  fnpr2ob  12983  fvprif  12986  2lgslem3  15342  2lgslem4  15344  bj-charfunbi  15457  pwle2  15643  subctctexmid  15645  pw1nct  15647  peano3nninf  15651  nninfsellemqall  15659  nninffeq  15664