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  2719  preq12bg  3541  ordsuc  4281  f1ocnv2d  5691  caucvgsrlemoffres  6865  prodge0  7796  un0addcl  8187  un0mulcl  8188  peano2uz2  8317  elfz2nn0  8940  fzind2  9062  expaddzap  9177  expmulzap  9179  cau3lem  9588  climuni  9691  climrecvg1n  9744  ialgcvga  9767
  Copyright terms: Public domain W3C validator