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

Theorem neii 2253
Description: Inference associated with df-ne 2252. (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 2252 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 143 1 ¬ 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1287  wne 2251
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 2252
This theorem is referenced by:  2dom  6455  updjudhcoinrg  6693  exmidomni  6719  exmidfodomrlemr  6749  exmidfodomrlemrALT  6750  ine0  7793  inelr  7979  xrltnr  9159  pnfnlt  9166  xrlttri3  9176  nltpnft  9188  3lcm2e6woprm  10862  6lcm4e12  10863  peano3nninf  11253  nninfsellemqall  11263
  Copyright terms: Public domain W3C validator