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  585  anandir  586  truantru  1396  falanfal  1399  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  sbnf2  1974  2eu4  2112  inidm  3336  ralidm  3515  opcom  4235  opeqsn  4237  poirr  4292  rnxpid  5045  xp11m  5049  fununi  5266  brprcneu  5489  erinxp  6587  dom2lem  6750  dmaddpi  7287  dmmulpi  7288  enq0ref  7395  enq0tr  7396  expap0  10506  sqap0  10542  xrmaxiflemcom  11212  gcddvds  11918  xmeter  13230
  Copyright terms: Public domain W3C validator