Theorem anidm 674

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anidmdbi  676  anandi  867  anandir  868  nannot  1445  truantru  1497  falanfal  1500  nic-axALT  1590  inidm  3784  opcom  4890  opeqsn  4892  poirr  4970  asymref2  5432  xp11  5488  fununi  5878  brprcneu  6096  f13dfv  6430  erinxp  7708  dom2lem  7881  pssnn  8063  dmaddpi  9591  dmmulpi  9592  gcddvds  15063  iscatd2  16165  dfiso2  16255  isnsg2  17447  eqger  17467  gaorber  17564  efgcpbllemb  17991  xmeter  22048  caucfil  22889  tgcgr4  25226  axcontlem5  25648  cusgra2v  25991  cusgra3v  25993  erclwwlkref  26341  erclwwlknref  26353  frgra3v  26529  disjunsn  28789  bnj594  30236  subfaclefac  30412  isbasisrelowllem1  32379  isbasisrelowllem2  32380  inixp  32693  cdlemg33b  35013  eelT11  37953  uunT11  38044  uunT11p1  38045  uunT11p2  38046  uun111  38053  2reu4a  39838  cplgr3v  40657  clwwlksn2  41217  erclwwlksref  41241  erclwwlksnref  41253  frgr3v  41445