Theorem anidm 564

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidmdbi  565  anandi  676  anandir  677  3anidm  1103  truantru  1573  falanfal  1576  nic-axALT  1674  inidm  4207  2reu4lem  4502  opcom  5481  poirr  5578  asymref2  6111  xp11  6169  fununi  6616  brprcneu  6871  brprcneuALT  6872  f13dfv  7272  erinxp  8810  dom2lem  9011  pssnn  9187  djuinf  10208  dmaddpi  10909  dmmulpi  10910  gcddvds  16527  iscatd2  17698  dfiso2  17790  isnsg2  19144  eqger  19166  gaorber  19296  efgcpbllemb  19741  xmeter  24377  caucfil  25240  tgcgr4  28515  axcontlem5  28952  cplgr3v  29419  erclwwlkref  30006  clwwlkn2  30030  erclwwlknref  30055  frgr3v  30261  numclwlk1lem1  30355  disjunsn  32580  bnj594  34948  subfaclefac  35203  isbasisrelowllem1  37378  isbasisrelowllem2  37379  inixp  37757  opideq  38366  cdlemg33b  40731  eelT11  44698  uunT11  44787  uunT11p1  44788  uunT11p2  44789  uun111  44796