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

Theorem anidm 396
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 395 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 132 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  anidmdbi  398  anandi  590  anandir  591  truantru  1412  falanfal  1415  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  sbnf2  1997  2eu4  2135  inidm  3368  ralidm  3547  opcom  4279  opeqsn  4281  poirr  4338  rnxpid  5100  xp11m  5104  fununi  5322  brprcneu  5547  erinxp  6663  dom2lem  6826  dmaddpi  7385  dmmulpi  7386  enq0ref  7493  enq0tr  7494  expap0  10640  sqap0  10677  xrmaxiflemcom  11392  gcddvds  12100  isnsg2  13273  eqger  13294  xmeter  14604
  Copyright terms: Public domain W3C validator