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

Theorem anidm 391
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 390 . 2 (𝜑 ↔ (𝜑𝜑))
21bicomi 131 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anidmdbi  393  anandi  562  anandir  563  truantru  1362  falanfal  1365  truxortru  1380  truxorfal  1381  falxortru  1382  falxorfal  1383  sbnf2  1932  2eu4  2068  inidm  3253  ralidm  3431  opcom  4140  opeqsn  4142  poirr  4197  rnxpid  4941  xp11m  4945  fununi  5159  brprcneu  5380  erinxp  6469  dom2lem  6632  dmaddpi  7097  dmmulpi  7098  enq0ref  7205  enq0tr  7206  expap0  10263  sqap0  10299  xrmaxiflemcom  10958  gcddvds  11548  xmeter  12500
  Copyright terms: Public domain W3C validator