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

Theorem impr 361
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
impr.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
impr  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem impr
StepHypRef Expression
1 impr.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 108 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 244 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  moi2  2722  preq12bg  3544  ordsuc  4287  f1ocnv2d  5704  caucvgsrlemoffres  6884  prodge0  7820  un0addcl  8215  un0mulcl  8216  peano2uz2  8345  elfz2nn0  8973  fzind2  9095  expaddzap  9299  expmulzap  9301  cau3lem  9710  climuni  9814  climrecvg1n  9867  ialgcvga  9890
  Copyright terms: Public domain W3C validator