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  1391  falanfal  1394  truxortru  1409  truxorfal  1410  falxortru  1411  falxorfal  1412  sbnf2  1969  2eu4  2107  inidm  3331  ralidm  3509  opcom  4228  opeqsn  4230  poirr  4285  rnxpid  5038  xp11m  5042  fununi  5256  brprcneu  5479  erinxp  6575  dom2lem  6738  dmaddpi  7266  dmmulpi  7267  enq0ref  7374  enq0tr  7375  expap0  10485  sqap0  10521  xrmaxiflemcom  11190  gcddvds  11896  xmeter  13076