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  1401  falanfal  1404  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  sbnf2  1981  2eu4  2119  inidm  3344  ralidm  3523  opcom  4250  opeqsn  4252  poirr  4307  rnxpid  5063  xp11m  5067  fununi  5284  brprcneu  5508  erinxp  6608  dom2lem  6771  dmaddpi  7323  dmmulpi  7324  enq0ref  7431  enq0tr  7432  expap0  10549  sqap0  10586  xrmaxiflemcom  11256  gcddvds  11963  isnsg2  13061  eqger  13081  xmeter  13906
  Copyright terms: Public domain W3C validator