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  554  anandir  555  truantru  1332  falanfal  1335  truxortru  1350  truxorfal  1351  falxortru  1352  falxorfal  1353  sbnf2  1898  2eu4  2034  inidm  3175  ralidm  3341  opcom  4005  opeqsn  4007  poirr  4062  rnxpid  4775  xp11m  4779  fununi  4987  brprcneu  5191  erinxp  6203  dom2lem  6275  dmaddpi  6515  dmmulpi  6516  enq0ref  6623  enq0tr  6624  expap0  9506  sqap0  9542  gcddvds  10355