Theorem anidm 396

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anidmdbi  398  anandi  590  anandir  591  truantru  1412  falanfal  1415  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  sbnf2  1993  2eu4  2131  inidm  3359  ralidm  3538  opcom  4271  opeqsn  4273  poirr  4328  rnxpid  5084  xp11m  5088  fununi  5306  brprcneu  5530  erinxp  6639  dom2lem  6802  dmaddpi  7359  dmmulpi  7360  enq0ref  7467  enq0tr  7468  expap0  10591  sqap0  10628  xrmaxiflemcom  11299  gcddvds  12006  isnsg2  13168  eqger  13189  xmeter  14422