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

Theorem anidm 376
Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
Assertion
Ref Expression
anidm ((φ φ) ↔ φ)

Proof of Theorem anidm
StepHypRef Expression
1 pm4.24 375 . 2 (φ ↔ (φ φ))
21bicomi 123 1 ((φ φ) ↔ φ)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anidmdbi  378  anandi  524  anandir  525  truantru  1289  falanfal  1292  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  sbnf2  1854  2eu4  1990  inidm  3140  ralidm  3315  opcom  3978  opeqsn  3980  poirr  4035  rnxpid  4698  xp11m  4702  fununi  4910  brprcneu  5114  erinxp  6116  dom2lem  6188  dmaddpi  6309  dmmulpi  6310  enq0ref  6415  enq0tr  6416  expap0  8919
  Copyright terms: Public domain W3C validator