Theorem anidm 575

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anidmdbi  576  anandi  689  anandir  690  3anidm  1121  truantru  1602  falanfal  1605  nic-axALT  1706  inidm  4126  2reu4lem  4482  opcom  5477  poirr  5575  asymref2  6117  xp11  6173  fununi  6626  brprcneu  6886  brprcneuALT  6887  f13dfv  7292  erinxp  8826  dom2lem  9033  pssnn  9198  djuinf  10280  dmaddpi  10988  dmmulpi  10989  gcddvds  16688  iscatd2  17870  dfiso2  17962  isnsg2  19381  eqger  19405  gaorber  19537  efgcpbllemb  19984  xmeter  24767  caucfil  25619  tgcgr4  29009  axcontlem5  29561  cplgr3v  30031  erclwwlkref  30626  clwwlkn2  30650  erclwwlknref  30675  frgr3v  30891  numclwlk1lem1  30985  disjunsn  33245  bnj594  35598  subfaclefac  36065  isbasisrelowllem1  38424  isbasisrelowllem2  38425  inixp  38808  opideq  39421  cdlemg33b  41910  eelT11  45834  uunT11  45923  uunT11p1  45924  uunT11p2  45925  uun111  45932