Theorem neii 2366

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

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

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 2365

This theorem is referenced by:  2dom  6861  updjudhcoinrg  7142  omp1eomlem  7155  nninfisol  7194  exmidomni  7203  mkvprop  7219  nninfwlporlemd  7233  nninfwlpoimlemginf  7237  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  ine0  8415  inelr  8605  xrltnr  9848  pnfnlt  9856  xrlttri3  9866  nltpnft  9883  xrpnfdc  9911  xrmnfdc  9912  xleaddadd  9956  zfz1iso  10915  3lcm2e6woprm  12227  6lcm4e12  12228  m1dvdsndvds  12389  unct  12602  fnpr2ob  12926  fvprif  12929  2lgslem3  15258  2lgslem4  15260  bj-charfunbi  15373  pwle2  15559  subctctexmid  15561  pw1nct  15563  peano3nninf  15567  nninfsellemqall  15575  nninffeq  15580