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

Theorem impr 376
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 114 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 255 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  reximddv2  2535  moi2  2860  preq12bg  3695  ordsuc  4473  f1ocnv2d  5967  supisoti  6890  caucvgsrlemoffres  7601  prodge0  8605  un0addcl  9003  un0mulcl  9004  peano2uz2  9151  elfz2nn0  9885  fzind2  10009  expaddzap  10330  expmulzap  10332  cau3lem  10879  climuni  11055  climrecvg1n  11110  fisumcom2  11200  dvdsval2  11485  algcvga  11721  lcmgcdlem  11747  divgcdcoprmex  11772  epttop  12248  cncnp  12388  cnconst  12392  bl2in  12561  metcnpi  12673  metcnpi2  12674  metcnpi3  12675
  Copyright terms: Public domain W3C validator