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  590  anandir  591  truantru  1421  falanfal  1424  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  sbnf2  2009  2eu4  2147  inidm  3382  ralidm  3561  opcom  4295  opeqsn  4297  poirr  4354  rnxpid  5117  xp11m  5121  fununi  5342  brprcneu  5569  erinxp  6696  dom2lem  6863  dmaddpi  7438  dmmulpi  7439  enq0ref  7546  enq0tr  7547  expap0  10714  sqap0  10751  xrmaxiflemcom  11560  gcddvds  12284  isnsg2  13539  eqger  13560  xmeter  14908