Theorem anidm 435

Description: Idempotent law for conjunction.

Assertion

Ref	Expression
anidm	⊢ ((φ ⋀ φ) ↔ φ)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm3.26 319	. 2 ⊢ ((φ ⋀ φ) → φ)
2		pm3.2 283	. . 3 ⊢ (φ → (φ → (φ ⋀ φ)))
3	2	pm2.43i 64	. 2 ⊢ (φ → (φ ⋀ φ))
4	1, 3	impbii 157	1 ⊢ ((φ ⋀ φ) ↔ φ)

Syntax hints:   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  pm4.24 436  anandi 513  anandir 514  nicodraw 956  2eu4 1457  inidm 2233  opeqsn 2818  poirr 2861  dmsnop 3344  asymref2 3456  xp11 3492  fununi 3579  fin 3667  th3qlem1 4332  dom2d 4422  pssnn 4554  dmaddpi 5038  dmmulpi 5039  lt2msqi 5895  cau3iri 6947  hlimcauii 9130  anidmdbi 10459

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain