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  1412  falanfal  1415  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  sbnf2  2000  2eu4  2138  inidm  3372  ralidm  3551  opcom  4283  opeqsn  4285  poirr  4342  rnxpid  5104  xp11m  5108  fununi  5326  brprcneu  5551  erinxp  6668  dom2lem  6831  dmaddpi  7392  dmmulpi  7393  enq0ref  7500  enq0tr  7501  expap0  10661  sqap0  10698  xrmaxiflemcom  11414  gcddvds  12130  isnsg2  13333  eqger  13354  xmeter  14672