ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anidm Unicode version

Theorem anidm 389
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
StepHypRef Expression
1 pm4.24 388 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 131 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anidmdbi  391  anandi  558  anandir  559  truantru  1338  falanfal  1341  truxortru  1356  truxorfal  1357  falxortru  1358  falxorfal  1359  sbnf2  1906  2eu4  2042  inidm  3210  ralidm  3386  opcom  4086  opeqsn  4088  poirr  4143  rnxpid  4878  xp11m  4882  fununi  5095  brprcneu  5311  erinxp  6380  dom2lem  6543  dmaddpi  6945  dmmulpi  6946  enq0ref  7053  enq0tr  7054  expap0  10046  sqap0  10082  gcddvds  11294
  Copyright terms: Public domain W3C validator