Theorem anidm 389

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 388	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 131	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anidmdbi  391  anandi  558  anandir  559  truantru  1338  falanfal  1341  truxortru  1356  truxorfal  1357  falxortru  1358  falxorfal  1359  sbnf2  1906  2eu4  2042  inidm  3212  ralidm  3388  opcom  4088  opeqsn  4090  poirr  4145  rnxpid  4880  xp11m  4884  fununi  5097  brprcneu  5313  erinxp  6382  dom2lem  6545  dmaddpi  6947  dmmulpi  6948  enq0ref  7055  enq0tr  7056  expap0  10048  sqap0  10084  gcddvds  11296