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  592  anandir  593  truantru  1443  falanfal  1446  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  sbnf2  2032  2eu4  2171  inidm  3413  ralidm  3592  opcom  4337  opeqsn  4339  poirr  4398  rnxpid  5163  xp11m  5167  fununi  5389  brprcneu  5620  erinxp  6756  dom2lem  6923  dmaddpi  7512  dmmulpi  7513  enq0ref  7620  enq0tr  7621  expap0  10791  sqap0  10828  xrmaxiflemcom  11760  gcddvds  12484  isnsg2  13740  eqger  13761  xmeter  15110