Theorem neii 2379

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

Syntax hints:  ¬ wn 3   = wceq 1373   ≠ wne 2377

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 2378

This theorem is referenced by:  2dom  6908  updjudhcoinrg  7195  omp1eomlem  7208  nninfisol  7247  exmidomni  7256  mkvprop  7272  nninfwlporlemd  7286  nninfwlpoimlemginf  7290  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  exmidaclem  7333  ine0  8479  inelr  8670  xrltnr  9914  pnfnlt  9922  xrlttri3  9932  nltpnft  9949  xrpnfdc  9977  xrmnfdc  9978  xleaddadd  10022  zfz1iso  10999  3lcm2e6woprm  12458  6lcm4e12  12459  m1dvdsndvds  12621  unct  12863  fnpr2ob  13222  fvprif  13225  2lgslem3  15628  2lgslem4  15630  bj-charfunbi  15861  pwle2  16050  subctctexmid  16052  pw1nct  16055  peano3nninf  16059  nninfsellemqall  16067  nninffeq  16072