Theorem anidm 393

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 392	. 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  395  anandi  579  anandir  580  truantru  1379  falanfal  1382  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  sbnf2  1956  2eu4  2092  inidm  3285  ralidm  3463  opcom  4172  opeqsn  4174  poirr  4229  rnxpid  4973  xp11m  4977  fununi  5191  brprcneu  5414  erinxp  6503  dom2lem  6666  dmaddpi  7133  dmmulpi  7134  enq0ref  7241  enq0tr  7242  expap0  10323  sqap0  10359  xrmaxiflemcom  11018  gcddvds  11652  xmeter  12605