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

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

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21ex 112 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 112 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  exp41  356  exp42  357  expl  364  exbiri  368  anasss  385  an31s  512  con4biddc  765  3impa  1110  exp516  1135  r19.29af2  2469  mpteqb  5289  dffo3  5342  fconstfvm  5407  fliftfun  5464  tfrlem1  5954  tfrlem9  5966  nnsucsssuc  6102  nnaordex  6131  diffifi  6382  prarloclemup  6651  genpcdl  6675  genpcuu  6676  recexap  7708  zaddcllemneg  8341  zdiv  8386  uzaddcl  8625  fz0fzelfz0  9086  fz0fzdiffz0  9089  elfzmlbp  9092  difelfzle  9094  fzo1fzo0n0  9141  ssfzo12bi  9183  modfzo0difsn  9345  expivallem  9421  expcllem  9431  expap0  9450  mulexp  9459  cjexp  9721  absexp  9906  divconjdvds  10161  addmodlteqALT  10171  divalglemeunn  10233  divalglemeuneg  10235  pw2dvdslemn  10253
  Copyright terms: Public domain W3C validator