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

Theorem neii 2257
Description: Inference associated with df-ne 2256. (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 2256 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 143 1 ¬ 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1289  wne 2255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-ne 2256
This theorem is referenced by:  2dom  6502  updjudhcoinrg  6751  exmidomni  6777  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  ine0  7851  inelr  8037  xrltnr  9219  pnfnlt  9226  xrlttri3  9236  nltpnft  9248  zfz1iso  10211  3lcm2e6woprm  11161  6lcm4e12  11162  peano3nninf  11554  nninfsellemqall  11564
  Copyright terms: Public domain W3C validator