Theorem anidm 331

Description: Idempotent law for conjunction. Theorem *4.24 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
anidm	|- ((ph /\ ph) <-> ph)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm3.26 256	. 2 |- ((ph /\ ph) -> ph)
2		pm3.2 232	. . 3 |- (ph -> (ph -> (ph /\ ph)))
3	2	pm2.43i 58	. 2 |- (ph -> (ph /\ ph))
4	1, 3	impbi 139	1 |- ((ph /\ ph) <-> ph)

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  anandi 392  anandir 393  pm5.74 442  euanv 1053  2eu4 1070  inidm 1649  poirr 2133  so 2152  dmsnop 2547  fununi 2705  fin 2770  th3qlem1 3250  dom2d 3307  pssnn 3428  dmaddpi 3812  dmmulpi 3813  lt2sq 4414  hlimcaui 5141

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org