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  1603  falanfal  1606  nic-axALT  1707  inidm  4172  2reu4lem  4479  opcom  5473  poirr  5571  asymref2  6111  xp11  6167  fununi  6615  brprcneu  6875  brprcneuALT  6876  f13dfv  7282  erinxp  8812  dom2lem  9019  pssnn  9184  djuinf  10267  dmaddpi  10975  dmmulpi  10976  gcddvds  16673  iscatd2  17855  dfiso2  17947  isnsg2  19366  eqger  19390  gaorber  19522  efgcpbllemb  19969  xmeter  24752  caucfil  25604  tgcgr4  28994  axcontlem5  29546  cplgr3v  30016  erclwwlkref  30611  clwwlkn2  30635  erclwwlknref  30660  frgr3v  30876  numclwlk1lem1  30970  disjunsn  33188  bnj594  35542  subfaclefac  35941  isbasisrelowllem1  38278  isbasisrelowllem2  38279  inixp  38662  opideq  39275  cdlemg33b  41764  eelT11  45688  uunT11  45777  uunT11p1  45778  uunT11p2  45779  uun111  45786