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

Theorem impr 371
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 113 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 253 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
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 is referenced by:  reximddv2  2466  moi2  2774  preq12bg  3567  ordsuc  4308  f1ocnv2d  5729  supisoti  6472  caucvgsrlemoffres  7027  prodge0  7988  un0addcl  8377  un0mulcl  8378  peano2uz2  8524  elfz2nn0  9194  fzind2  9314  expaddzap  9606  expmulzap  9608  cau3lem  10127  climuni  10259  climrecvg1n  10312  dvdsval2  10332  ialgcvga  10566  lcmgcdlem  10592  divgcdcoprmex  10617
  Copyright terms: Public domain W3C validator