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 951  2eu4 1452  inidm 2220  opeqsn 2799  poirr 2842  dmsnop 3325  asymref2 3437  xp11 3473  fununi 3560  fin 3648  th3qlem1 4311  dom2d 4398  pssnn 4526  dmaddpi 5005  dmmulpi 5006  lt2msq 5843  cau3ir 6881  hlimcaui 9094  anidmdbi 10427

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