Theorem anidm 675

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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 386

This theorem is referenced by:  anidmdbi  677  anandi  870  anandir  871  nannot  1451  truantru  1504  falanfal  1507  nic-axALT  1597  inidm  3814  opcom  4955  opeqsn  4957  poirr  5036  asymref2  5501  xp11  5557  fununi  5952  brprcneu  6171  f13dfv  6515  erinxp  7806  dom2lem  7980  pssnn  8163  dmaddpi  9697  dmmulpi  9698  gcddvds  15206  iscatd2  16323  dfiso2  16413  isnsg2  17605  eqger  17625  gaorber  17722  efgcpbllemb  18149  xmeter  22219  caucfil  23062  tgcgr4  25407  axcontlem5  25829  cplgr3v  26312  clwwlksn2  26890  erclwwlksref  26914  erclwwlksnref  26926  frgr3v  27119  disjunsn  29379  bnj594  30956  subfaclefac  31132  isbasisrelowllem1  33174  isbasisrelowllem2  33175  inixp  33494  cdlemg33b  35814  eelT11  38752  uunT11  38843  uunT11p1  38844  uunT11p2  38845  uun111  38852  2reu4a  40952