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

Theorem anidm 393
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 392 . 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  395  anandi  564  anandir  565  truantru  1364  falanfal  1367  truxortru  1382  truxorfal  1383  falxortru  1384  falxorfal  1385  sbnf2  1934  2eu4  2070  inidm  3255  ralidm  3433  opcom  4142  opeqsn  4144  poirr  4199  rnxpid  4943  xp11m  4947  fununi  5161  brprcneu  5382  erinxp  6471  dom2lem  6634  dmaddpi  7101  dmmulpi  7102  enq0ref  7209  enq0tr  7210  expap0  10291  sqap0  10327  xrmaxiflemcom  10986  gcddvds  11579  xmeter  12532
  Copyright terms: Public domain W3C validator