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  1997  2eu4  2135  inidm  3369  ralidm  3548  opcom  4280  opeqsn  4282  poirr  4339  rnxpid  5101  xp11m  5105  fununi  5323  brprcneu  5548  erinxp  6665  dom2lem  6828  dmaddpi  7387  dmmulpi  7388  enq0ref  7495  enq0tr  7496  expap0  10643  sqap0  10680  xrmaxiflemcom  11395  gcddvds  12103  isnsg2  13276  eqger  13297  xmeter  14615