NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  anidm GIF version

Theorem anidm 625
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 624 . 2 (φ ↔ (φ φ))
21bicomi 193 1 ((φ φ) ↔ φ)
Colors of variables: wff setvar class
Syntax hints:  wb 176   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  anidmdbi  627  anandi  801  anandir  802  nannot  1293  truantru  1336  falanfal  1339  nic-axALT  1439  sbnf2  2108  2eu4  2287  elcomplg  3218  inidm  3464  ncfinlower  4483  nnpw1ex  4484  nnpweq  4523  phialllem1  4616  xp11  5056  fununi  5160
  Copyright terms: Public domain W3C validator