Theorem anidm 388

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

Syntax hints:   /\ wa 102   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anidmdbi  390  anandi  555  anandir  556  truantru  1333  falanfal  1336  truxortru  1351  truxorfal  1352  falxortru  1353  falxorfal  1354  sbnf2  1899  2eu4  2035  inidm  3182  ralidm  3349  opcom  4013  opeqsn  4015  poirr  4070  rnxpid  4785  xp11m  4789  fununi  4998  brprcneu  5202  erinxp  6246  dom2lem  6319  dmaddpi  6577  dmmulpi  6578  enq0ref  6685  enq0tr  6686  expap0  9603  sqap0  9639  gcddvds  10499