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  592  anandir  593  truantru  1443  falanfal  1446  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  sbnf2  2032  2eu4  2171  inidm  3413  ralidm  3592  opcom  4338  opeqsn  4340  poirr  4399  rnxpid  5166  xp11m  5170  fununi  5392  brprcneu  5625  erinxp  6769  dom2lem  6936  dmaddpi  7528  dmmulpi  7529  enq0ref  7636  enq0tr  7637  expap0  10808  sqap0  10845  xrmaxiflemcom  11781  gcddvds  12505  isnsg2  13761  eqger  13782  xmeter  15131  clwwlkn2  16189