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  1401  falanfal  1404  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  sbnf2  1981  2eu4  2119  inidm  3344  ralidm  3523  opcom  4248  opeqsn  4250  poirr  4305  rnxpid  5060  xp11m  5064  fununi  5281  brprcneu  5505  erinxp  6604  dom2lem  6767  dmaddpi  7319  dmmulpi  7320  enq0ref  7427  enq0tr  7428  expap0  10543  sqap0  10579  xrmaxiflemcom  11248  gcddvds  11954  xmeter  13718