Theorem anidm 400

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 399	. 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  402  anandi  598  anandir  599  truantru  1450  falanfal  1453  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  sbnf2  2041  2eu4  2180  inidm  3440  ralidm  3625  opcom  4386  opeqsn  4388  poirr  4447  rnxpid  5217  xp11m  5221  fununi  5444  brprcneu  5683  erinxp  6873  dom2lem  7048  dmaddpi  7682  dmmulpi  7683  enq0ref  7790  enq0tr  7791  msqap0  8986  expap0  10984  sqap0  11021  xrmaxiflemcom  11993  gcddvds  12718  isnsg2  13983  eqger  14004  xmeter  15460  clwwlkn2  16576