Theorem anidm 394

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 393	. 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anidmdbi  396  anandi  580  anandir  581  truantru  1380  falanfal  1383  truxortru  1398  truxorfal  1399  falxortru  1400  falxorfal  1401  sbnf2  1957  2eu4  2093  inidm  3290  ralidm  3468  opcom  4180  opeqsn  4182  poirr  4237  rnxpid  4981  xp11m  4985  fununi  5199  brprcneu  5422  erinxp  6511  dom2lem  6674  dmaddpi  7157  dmmulpi  7158  enq0ref  7265  enq0tr  7266  expap0  10354  sqap0  10390  xrmaxiflemcom  11050  gcddvds  11688  xmeter  12644