Theorem anidm 389

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 388	. 2 |- ( ph <-> ( ph /\ ph ) )
2	1	bicomi 131	1 |- ( ( ph /\ ph ) <-> ph )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anidmdbi  391  anandi  558  anandir  559  truantru  1338  falanfal  1341  truxortru  1356  truxorfal  1357  falxortru  1358  falxorfal  1359  sbnf2  1906  2eu4  2042  inidm  3210  ralidm  3386  opcom  4086  opeqsn  4088  poirr  4143  rnxpid  4878  xp11m  4882  fununi  5095  brprcneu  5311  erinxp  6380  dom2lem  6543  dmaddpi  6945  dmmulpi  6946  enq0ref  7053  enq0tr  7054  expap0  10046  sqap0  10082  gcddvds  11294