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 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3628  opcom  4391  opeqsn  4393  poirr  4452  rnxpid  5222  xp11m  5226  fununi  5449  brprcneu  5688  erinxp  6883  dom2lem  7058  dmaddpi  7692  dmmulpi  7693  enq0ref  7800  enq0tr  7801  msqap0  8998  expap0  11019  sqap0  11056  xrmaxiflemcom  12031  gcddvds  12756  isnsg2  14055  eqger  14076  xmeter  15586  clwwlkn2  16760  2alsraln0idm  17257