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  1420  falanfal  1423  truxortru  1438  truxorfal  1439  falxortru  1440  falxorfal  1441  sbnf2  2008  2eu4  2146  inidm  3381  ralidm  3560  opcom  4294  opeqsn  4296  poirr  4353  rnxpid  5116  xp11m  5120  fununi  5341  brprcneu  5568  erinxp  6695  dom2lem  6862  dmaddpi  7437  dmmulpi  7438  enq0ref  7545  enq0tr  7546  expap0  10712  sqap0  10749  xrmaxiflemcom  11531  gcddvds  12255  isnsg2  13510  eqger  13531  xmeter  14879