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  1446  falanfal  1449  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  sbnf2  2035  2eu4  2174  inidm  3430  ralidm  3610  opcom  4367  opeqsn  4369  poirr  4428  rnxpid  5197  xp11m  5201  fununi  5424  brprcneu  5663  erinxp  6843  dom2lem  7011  dmaddpi  7640  dmmulpi  7641  enq0ref  7748  enq0tr  7749  expap0  10931  sqap0  10968  xrmaxiflemcom  11934  gcddvds  12659  isnsg2  13920  eqger  13941  xmeter  15301  clwwlkn2  16416