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

Theorem expr 357
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
expr  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 347 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 115 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:  rexlimdvaa  2431  issod  4053  ordsuc  4281  fcof1  5410  riota5f  5479  ovmpt2df  5619  tfrlemi1  5933  addnq0mo  6526  mulnq0mo  6527  genprndl  6600  genprndu  6601  addlocpr  6615  ltexprlemm  6679  ltexprlemopl  6680  ltexprlemopu  6682  ltexprlemfl  6688  ltexprlemfu  6690  aptiprleml  6718  caucvgprprlemexbt  6785  addsrmo  6809  mulsrmo  6810  prodge0  7796  un0addcl  8187  un0mulcl  8188  iseqfveq2  9106  iseqshft2  9110  monoord  9113  iseqsplit  9116  expnegzap  9167  caucvgrelemcau  9457  cau3lem  9588
  Copyright terms: Public domain W3C validator