Theorem anidm 677

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

Syntax hints:   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  anidmdbi  679  anandi  888  anandir  889  nannot  1493  truantru  1546  falanfal  1549  nic-axALT  1639  inidm  3855  opcom  4994  opeqsn  4996  poirr  5075  asymref2  5548  xp11  5604  fununi  6002  brprcneu  6222  f13dfv  6570  erinxp  7864  dom2lem  8037  pssnn  8219  dmaddpi  9750  dmmulpi  9751  gcddvds  15272  iscatd2  16389  dfiso2  16479  isnsg2  17671  eqger  17691  gaorber  17787  efgcpbllemb  18214  xmeter  22285  caucfil  23127  tgcgr4  25471  axcontlem5  25893  cplgr3v  26387  erclwwlkref  26977  clwwlkn2  27007  erclwwlknref  27033  frgr3v  27255  disjunsn  29533  bnj594  31108  subfaclefac  31284  isbasisrelowllem1  33333  isbasisrelowllem2  33334  inixp  33653  opideq  34250  cdlemg33b  36312  eelT11  39249  uunT11  39340  uunT11p1  39341  uunT11p2  39342  uun111  39349  2reu4a  41510