Theorem anidm 434

Description: Idempotent law for conjunction.

Assertion

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

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm3.26 319	. 2 |- ((ph /\ ph) -> ph)
2		pm3.2 283	. . 3 |- (ph -> (ph -> (ph /\ ph)))
3	2	pm2.43i 64	. 2 |- (ph -> (ph /\ ph))
4	1, 3	impbi 157	1 |- ((ph /\ ph) <-> ph)

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.24 435  anandi 512  anandir 513  nicodraw 954  2eu4 1455  inidm 2226  opeqsn 2809  poirr 2852  dmsnop 3335  asymref2 3447  xp11 3483  fununi 3570  fin 3658  th3qlem1 4321  dom2d 4411  pssnn 4546  dmaddpi 5037  dmmulpi 5038  lt2msq 5890  cau3ir 6922  hlimcaui 9108  anidmdbi 10437

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