Theorem anidm 568

Description: Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Assertion

Ref	Expression
anidm	⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm4.24 567	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 227	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  anidmdbi  569  anandi  676  anandir  677  3anidm  1106  truantru  1576  falanfal  1579  nic-axALT  1682  inidm  4133  2reu4lem  4437  opcom  5384  poirr  5480  asymref2  5982  xp11  6038  fununi  6455  brprcneu  6708  fvprc  6709  f13dfv  7085  erinxp  8473  dom2lem  8668  pssnn  8846  pssnnOLD  8895  djuinf  9802  dmaddpi  10504  dmmulpi  10505  gcddvds  16062  iscatd2  17184  dfiso2  17277  isnsg2  18572  eqger  18594  gaorber  18702  efgcpbllemb  19145  xmeter  23331  caucfil  24180  tgcgr4  26622  axcontlem5  27059  cplgr3v  27523  erclwwlkref  28103  clwwlkn2  28127  erclwwlknref  28152  frgr3v  28358  numclwlk1lem1  28452  disjunsn  30652  bnj594  32605  subfaclefac  32851  isbasisrelowllem1  35263  isbasisrelowllem2  35264  inixp  35623  opideq  36215  cdlemg33b  38458  eelT11  42000  uunT11  42089  uunT11p1  42090  uunT11p2  42091  uun111  42098