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

Theorem neii 2287
Description: Inference associated with df-ne 2286. (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 2286 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 144 1 ¬ 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1316  wne 2285
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 2286
This theorem is referenced by:  2dom  6667  updjudhcoinrg  6934  omp1eomlem  6947  exmidomni  6982  mkvprop  7000  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  ine0  8124  inelr  8314  xrltnr  9534  pnfnlt  9541  xrlttri3  9551  nltpnft  9565  xrpnfdc  9593  xrmnfdc  9594  xleaddadd  9638  zfz1iso  10552  3lcm2e6woprm  11694  6lcm4e12  11695  unct  11881  pwle2  13120  subctctexmid  13123  peano3nninf  13128  nninfsellemqall  13138  nninffeq  13143
  Copyright terms: Public domain W3C validator