Theorem anidm 393

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 392	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 131	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anidmdbi  395  anandi  579  anandir  580  truantru  1379  falanfal  1382  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  sbnf2  1954  2eu4  2090  inidm  3280  ralidm  3458  opcom  4167  opeqsn  4169  poirr  4224  rnxpid  4968  xp11m  4972  fununi  5186  brprcneu  5407  erinxp  6496  dom2lem  6659  dmaddpi  7126  dmmulpi  7127  enq0ref  7234  enq0tr  7235  expap0  10316  sqap0  10352  xrmaxiflemcom  11011  gcddvds  11641  xmeter  12594