Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  neii GIF version

Theorem neii 2326
 Description: Inference associated with df-ne 2325. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neii.1 𝐴𝐵
Assertion
Ref Expression
neii ¬ 𝐴 = 𝐵

Proof of Theorem neii
StepHypRef Expression
1 neii.1 . 2 𝐴𝐵
2 df-ne 2325 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 144 1 ¬ 𝐴 = 𝐵
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   = wceq 1332   ≠ wne 2324 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 2325 This theorem is referenced by:  2dom  6739  updjudhcoinrg  7011  omp1eomlem  7024  exmidomni  7064  mkvprop  7080  exmidfodomrlemr  7116  exmidfodomrlemrALT  7117  exmidaclem  7122  ine0  8248  inelr  8438  xrltnr  9664  pnfnlt  9672  xrlttri3  9682  nltpnft  9696  xrpnfdc  9724  xrmnfdc  9725  xleaddadd  9769  zfz1iso  10689  3lcm2e6woprm  11934  6lcm4e12  11935  unct  12122  bj-charfunbi  13324  pwle2  13509  subctctexmid  13512  pw1nct  13514  peano3nninf  13519  nninfsellemqall  13528  nninffeq  13533
 Copyright terms: Public domain W3C validator