Theorem anidm 376

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

Step	Hyp	Ref	Expression
1		pm4.24 375	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 123	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anidmdbi  378  anandi  524  anandir  525  truantru  1292  falanfal  1295  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  sbnf2  1857  2eu4  1993  inidm  3146  ralidm  3321  opcom  3987  opeqsn  3989  poirr  4044  rnxpid  4755  xp11m  4759  fununi  4967  brprcneu  5171  erinxp  6180  dom2lem  6252  dmaddpi  6423  dmmulpi  6424  enq0ref  6531  enq0tr  6532  expap0  9285  sqap0  9320