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

Theorem anidm 394
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 393 . 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  396  anandi  580  anandir  581  truantru  1383  falanfal  1386  truxortru  1401  truxorfal  1402  falxortru  1403  falxorfal  1404  sbnf2  1961  2eu4  2099  inidm  3317  ralidm  3495  opcom  4213  opeqsn  4215  poirr  4270  rnxpid  5023  xp11m  5027  fununi  5241  brprcneu  5464  erinxp  6557  dom2lem  6720  dmaddpi  7248  dmmulpi  7249  enq0ref  7356  enq0tr  7357  expap0  10459  sqap0  10495  xrmaxiflemcom  11158  gcddvds  11863  xmeter  12932
  Copyright terms: Public domain W3C validator