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  594  anandir  595  truantru  1445  falanfal  1448  truxortru  1463  truxorfal  1464  falxortru  1465  falxorfal  1466  sbnf2  2034  2eu4  2173  inidm  3416  ralidm  3595  opcom  4343  opeqsn  4345  poirr  4404  rnxpid  5171  xp11m  5175  fununi  5398  brprcneu  5632  erinxp  6778  dom2lem  6945  dmaddpi  7545  dmmulpi  7546  enq0ref  7653  enq0tr  7654  expap0  10832  sqap0  10869  xrmaxiflemcom  11827  gcddvds  12552  isnsg2  13808  eqger  13829  xmeter  15179  clwwlkn2  16291