Theorem anidm 565

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anidmdbi  566  anandi  672  anandir  673  3anidm  1095  truantru  1553  falanfal  1556  nic-axALT  1654  inidm  4110  2reu4lem  4373  opcom  5275  poirr  5365  asymref2  5845  xp11  5900  fununi  6291  brprcneu  6522  f13dfv  6887  erinxp  8212  dom2lem  8387  pssnn  8572  djuinf  9449  dmaddpi  10147  dmmulpi  10148  gcddvds  15673  iscatd2  16769  dfiso2  16859  isnsg2  18051  eqger  18071  gaorber  18167  efgcpbllemb  18596  xmeter  22714  caucfil  23557  tgcgr4  25987  axcontlem5  26425  cplgr3v  26888  erclwwlkref  27473  clwwlkn2  27497  erclwwlknref  27523  frgr3v  27734  numclwlk1lem1  27828  disjunsn  30010  bnj594  31756  subfaclefac  31987  isbasisrelowllem1  34113  isbasisrelowllem2  34114  inixp  34481  opideq  35082  cdlemg33b  37324  eelT11  40532  uunT11  40621  uunT11p1  40622  uunT11p2  40623  uun111  40630