Theorem anidm 376

Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Assertion

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

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm4.24 375	. 2 |- (ph <-> (ph /\ ph))
2	1	bicomi 123	1 |- ((ph /\ ph) <-> ph)

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anidmdbi  378  anandi  524  anandir  525  truantru  1289  falanfal  1292  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  sbnf2  1854  2eu4  1990  inidm  3140  ralidm  3315  opcom  3978  opeqsn  3980  poirr  4035  rnxpid  4698  xp11m  4702  fununi  4910  brprcneu  5114  erinxp  6116  dom2lem  6188  dmaddpi  6309  dmmulpi  6310  enq0ref  6416  enq0tr  6417  expap0  8939