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

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
StepHypRef Expression
1 pm4.24 387 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 130 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator