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  1421  falanfal  1424  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  sbnf2  2010  2eu4  2149  inidm  3390  ralidm  3569  opcom  4313  opeqsn  4315  poirr  4372  rnxpid  5136  xp11m  5140  fununi  5361  brprcneu  5592  erinxp  6719  dom2lem  6886  dmaddpi  7473  dmmulpi  7474  enq0ref  7581  enq0tr  7582  expap0  10751  sqap0  10788  xrmaxiflemcom  11675  gcddvds  12399  isnsg2  13654  eqger  13675  xmeter  15023