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

Theorem impr 379
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 115 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 257 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
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 is referenced by:  reximddv2  2582  moi2  2920  preq12bg  3775  ordsuc  4564  f1ocnv2d  6078  supisoti  7012  caucvgsrlemoffres  7802  prodge0  8814  un0addcl  9212  un0mulcl  9213  peano2uz2  9363  elfz2nn0  10115  fzind2  10242  expaddzap  10567  expmulzap  10569  cau3lem  11126  climuni  11304  climrecvg1n  11359  fisumcom2  11449  fprodcom2fi  11637  dvdsval2  11800  algcvga  12054  lcmgcdlem  12080  divgcdcoprmex  12105  prmpwdvds  12356  isgrpinv  12935  dvdsrcl2  13306  islss4  13507  lspsnel6  13533  epttop  13778  cncnp  13918  cnconst  13922  bl2in  14091  metcnpi  14203  metcnpi2  14204  metcnpi3  14205
  Copyright terms: Public domain W3C validator