Theorem anidm 432

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 433  anandi 510  anandir 511  nicodraw 950  2eu4 1450  inidm 2218  opeqsn 2797  poirr 2840  dmsnop 3323  asymref2 3432  xp11 3468  fununi 3555  fin 3642  th3qlem1 4304  dom2d 4391  pssnn 4519  dmaddpi 4998  dmmulpi 4999  lt2msq 5837  cau3ir 6860  hlimcaui 9045  anidmdbi 10370

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