Theorem anidm 400

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anidmdbi  402  anandi  598  anandir  599  truantru  1450  falanfal  1453  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  sbnf2  2041  2eu4  2180  inidm  3440  ralidm  3628  opcom  4391  opeqsn  4393  poirr  4452  rnxpid  5222  xp11m  5226  fununi  5449  brprcneu  5688  erinxp  6883  dom2lem  7058  dmaddpi  7693  dmmulpi  7694  enq0ref  7801  enq0tr  7802  msqap0  8999  expap0  11021  sqap0  11058  xrmaxiflemcom  12034  gcddvds  12759  isnsg2  14059  eqger  14080  xmeter  15628  clwwlkn2  16828  2alsraln0idm  17326