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

Theorem nesymi 2386
Description: Inference associated with nesym 2385. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
nesymi.1 𝐴𝐵
Assertion
Ref Expression
nesymi ¬ 𝐵 = 𝐴

Proof of Theorem nesymi
StepHypRef Expression
1 nesymi.1 . 2 𝐴𝐵
2 nesym 2385 . 2 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
31, 2mpbi 144 1 ¬ 𝐵 = 𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1348  wne 2340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341
This theorem is referenced by:  frec0g  6376  djune  7055  omp1eomlem  7071  fodjum  7122  fodju0  7123  ismkvnex  7131  mkvprop  7134  omniwomnimkv  7143  3nelsucpw1  7211  xrltnr  9736  nltmnf  9745  xnn0xadd0  9824  pwle2  14031  nninfalllem1  14041  nninfall  14042  nninfsellemeq  14047  trirec0xor  14077
  Copyright terms: Public domain W3C validator