Theorem neii 2337

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

Syntax hints:  ¬ wn 3   = wceq 1343   ≠ wne 2335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-ne 2336

This theorem is referenced by:  2dom  6767  updjudhcoinrg  7042  omp1eomlem  7055  nninfisol  7093  exmidomni  7102  mkvprop  7118  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  ine0  8288  inelr  8478  xrltnr  9711  pnfnlt  9719  xrlttri3  9729  nltpnft  9746  xrpnfdc  9774  xrmnfdc  9775  xleaddadd  9819  zfz1iso  10750  3lcm2e6woprm  12014  6lcm4e12  12015  m1dvdsndvds  12176  unct  12371  bj-charfunbi  13653  pwle2  13838  subctctexmid  13841  pw1nct  13843  peano3nninf  13847  nninfsellemqall  13855  nninffeq  13860