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

Theorem anidm 382
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 381 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 127 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  anidmdbi  384  anandi  532  anandir  533  truantru  1308  falanfal  1311  truxortru  1326  truxorfal  1327  falxortru  1328  falxorfal  1329  sbnf2  1873  2eu4  2009  inidm  3174  ralidm  3349  opcom  4015  opeqsn  4017  poirr  4072  rnxpid  4783  xp11m  4787  fununi  4995  brprcneu  5199  erinxp  6211  dom2lem  6283  dmaddpi  6481  dmmulpi  6482  enq0ref  6589  enq0tr  6590  expap0  9450  sqap0  9486
  Copyright terms: Public domain W3C validator