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  594  anandir  595  truantru  1445  falanfal  1448  truxortru  1463  truxorfal  1464  falxortru  1465  falxorfal  1466  sbnf2  2034  2eu4  2173  inidm  3416  ralidm  3595  opcom  4343  opeqsn  4345  poirr  4404  rnxpid  5171  xp11m  5175  fununi  5398  brprcneu  5632  erinxp  6777  dom2lem  6944  dmaddpi  7544  dmmulpi  7545  enq0ref  7652  enq0tr  7653  expap0  10830  sqap0  10867  xrmaxiflemcom  11809  gcddvds  12533  isnsg2  13789  eqger  13810  xmeter  15159  clwwlkn2  16271