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

Theorem 3anidm12 1305
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
Hypothesis
Ref Expression
3anidm12.1  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3anidm12  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem 3anidm12
StepHypRef Expression
1 3anidm12.1 . . 3  |-  ( (
ph  /\  ph  /\  ps )  ->  ch )
213expib 1207 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
32anabsi5 579 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 979
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  df-3an 981
This theorem is referenced by:  3anidm13  1306  syl2an3an  1308  prarloclemarch2  7431  nq02m  7477  recexprlem1ssl  7645  recexprlem1ssu  7646  nncan  8199  dividap  8671  modqid0  10363  sqdividap  10598  subsq  10640  retanclap  11743  tannegap  11749  gcd0id  11993  coprm  12157
  Copyright terms: Public domain W3C validator