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  3414  ralidm  3593  opcom  4341  opeqsn  4343  poirr  4402  rnxpid  5169  xp11m  5173  fununi  5395  brprcneu  5628  erinxp  6773  dom2lem  6940  dmaddpi  7535  dmmulpi  7536  enq0ref  7643  enq0tr  7644  expap0  10821  sqap0  10858  xrmaxiflemcom  11800  gcddvds  12524  isnsg2  13780  eqger  13801  xmeter  15150  clwwlkn2  16216