Theorem neii 2402

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

Syntax hints:  ¬ wn 3   = wceq 1395   ≠ wne 2400

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 2401

This theorem is referenced by:  2dom  6948  updjudhcoinrg  7236  omp1eomlem  7249  nninfisol  7288  exmidomni  7297  mkvprop  7313  nninfwlporlemd  7327  nninfwlpoimlemginf  7331  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  exmidaclem  7378  ine0  8528  inelr  8719  xrltnr  9963  pnfnlt  9971  xrlttri3  9981  nltpnft  9998  xrpnfdc  10026  xrmnfdc  10027  xleaddadd  10071  zfz1iso  11050  3lcm2e6woprm  12594  6lcm4e12  12595  m1dvdsndvds  12757  unct  12999  fnpr2ob  13359  fvprif  13362  2lgslem3  15765  2lgslem4  15767  bj-charfunbi  16104  pwle2  16295  subctctexmid  16297  pw1nct  16300  peano3nninf  16304  nninfsellemqall  16312  nninffeq  16317