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

Theorem exp32 365
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
exp32  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21ex 115 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32expd 258 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-ia3 108
This theorem is referenced by:  exp44  373  exp45  374  expr  375  anassrs  400  an13s  567  3impb  1199  xordidc  1399  f0rn0  5410  funfvima3  5750  isoini  5818  ovg  6012  fundmen  6805  distrlem1prl  7580  distrlem1pru  7581  caucvgprprlemaddq  7706  recexgt0sr  7771  axpre-suploclemres  7899  cnegexlem2  8132  mulgt1  8819  faclbnd  10720  divgcdcoprm0  12100  cncongr2  12103  oddpwdclemdvds  12169  oddpwdclemndvds  12170  infpnlem1  12356  cnpnei  13689  zabsle1  14370
  Copyright terms: Public domain W3C validator