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

Theorem impr 372
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 254 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  reximddv2  2479  moi2  2799  preq12bg  3625  ordsuc  4394  f1ocnv2d  5864  supisoti  6761  caucvgsrlemoffres  7408  prodge0  8378  un0addcl  8769  un0mulcl  8770  peano2uz2  8916  elfz2nn0  9589  fzind2  9713  expaddzap  10062  expmulzap  10064  cau3lem  10610  climuni  10744  climrecvg1n  10800  fisumcom2  10895  dvdsval2  11140  algcvga  11374  lcmgcdlem  11400  divgcdcoprmex  11425  epttop  11853
  Copyright terms: Public domain W3C validator