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  585  anandir  586  truantru  1396  falanfal  1399  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  sbnf2  1974  2eu4  2112  inidm  3336  ralidm  3515  opcom  4235  opeqsn  4237  poirr  4292  rnxpid  5045  xp11m  5049  fununi  5266  brprcneu  5489  erinxp  6587  dom2lem  6750  dmaddpi  7287  dmmulpi  7288  enq0ref  7395  enq0tr  7396  expap0  10506  sqap0  10542  xrmaxiflemcom  11212  gcddvds  11918  xmeter  13230