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

Theorem neii 2285
Description: Inference associated with df-ne 2284. (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 2284 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 144 1 ¬ 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1314  wne 2283
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 2284
This theorem is referenced by:  2dom  6665  updjudhcoinrg  6932  omp1eomlem  6945  exmidomni  6980  mkvprop  6998  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  ine0  8120  inelr  8309  xrltnr  9506  pnfnlt  9513  xrlttri3  9523  nltpnft  9537  xrpnfdc  9565  xrmnfdc  9566  xleaddadd  9610  zfz1iso  10524  3lcm2e6woprm  11663  6lcm4e12  11664  unct  11849  pwle2  13016  subctctexmid  13019  peano3nninf  13024  nninfsellemqall  13034  nninffeq  13039
  Copyright terms: Public domain W3C validator