Theorem anidm 394

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 393	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 131	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anidmdbi  396  anandi  580  anandir  581  truantru  1383  falanfal  1386  truxortru  1401  truxorfal  1402  falxortru  1403  falxorfal  1404  sbnf2  1961  2eu4  2099  inidm  3317  ralidm  3495  opcom  4213  opeqsn  4215  poirr  4270  rnxpid  5023  xp11m  5027  fununi  5241  brprcneu  5464  erinxp  6557  dom2lem  6720  dmaddpi  7248  dmmulpi  7249  enq0ref  7356  enq0tr  7357  expap0  10459  sqap0  10495  xrmaxiflemcom  11158  gcddvds  11863  xmeter  12932