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  4336  opeqsn  4338  poirr  4397  rnxpid  5162  xp11m  5166  fununi  5388  brprcneu  5619  erinxp  6754  dom2lem  6921  dmaddpi  7508  dmmulpi  7509  enq0ref  7616  enq0tr  7617  expap0  10786  sqap0  10823  xrmaxiflemcom  11755  gcddvds  12479  isnsg2  13735  eqger  13756  xmeter  15104