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

Theorem nesymi 2373
Description: Inference associated with nesym 2372. (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 2372 . 2 (𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
31, 2mpbi 144 1 ¬ 𝐵 = 𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1335  wne 2327
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 604  ax-in2 605  ax-5 1427  ax-gen 1429  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-ne 2328
This theorem is referenced by:  frec0g  6344  djune  7022  omp1eomlem  7038  fodjum  7089  fodju0  7090  ismkvnex  7098  mkvprop  7101  omniwomnimkv  7110  3nelsucpw1  7169  xrltnr  9686  nltmnf  9695  xnn0xadd0  9771  pwle2  13581  nninfalllem1  13591  nninfall  13592  nninfsellemeq  13597  trirec0xor  13627
  Copyright terms: Public domain W3C validator