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  3413  ralidm  3592  opcom  4337  opeqsn  4339  poirr  4398  rnxpid  5163  xp11m  5167  fununi  5389  brprcneu  5622  erinxp  6764  dom2lem  6931  dmaddpi  7523  dmmulpi  7524  enq0ref  7631  enq0tr  7632  expap0  10803  sqap0  10840  xrmaxiflemcom  11775  gcddvds  12499  isnsg2  13755  eqger  13776  xmeter  15125