Theorem anidm 396

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anidmdbi  398  anandi  594  anandir  595  truantru  1446  falanfal  1449  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  sbnf2  2037  2eu4  2176  inidm  3434  ralidm  3614  opcom  4372  opeqsn  4374  poirr  4433  rnxpid  5202  xp11m  5206  fununi  5429  brprcneu  5668  erinxp  6856  dom2lem  7024  dmaddpi  7656  dmmulpi  7657  enq0ref  7764  enq0tr  7765  expap0  10955  sqap0  10992  xrmaxiflemcom  11959  gcddvds  12684  isnsg2  13956  eqger  13977  xmeter  15427  clwwlkn2  16542