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

Theorem anidm 396
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 395 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 132 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  anidmdbi  398  anandi  590  anandir  591  truantru  1412  falanfal  1415  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  sbnf2  1993  2eu4  2131  inidm  3359  ralidm  3538  opcom  4268  opeqsn  4270  poirr  4325  rnxpid  5081  xp11m  5085  fununi  5303  brprcneu  5527  erinxp  6635  dom2lem  6798  dmaddpi  7354  dmmulpi  7355  enq0ref  7462  enq0tr  7463  expap0  10581  sqap0  10618  xrmaxiflemcom  11289  gcddvds  11996  isnsg2  13142  eqger  13163  xmeter  14393
  Copyright terms: Public domain W3C validator