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

Theorem exp31 356
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 113 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 113 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  exp41  362  exp42  363  expl  370  exbiri  374  anasss  391  an31s  537  con4biddc  792  3impa  1138  exp516  1163  r19.29af2  2508  disjiun  3840  mpteqb  5393  dffo3  5446  fconstfvm  5515  fliftfun  5575  tfrlem1  6073  tfrlem9  6084  tfr1onlemaccex  6113  tfrcllemaccex  6126  tfrcl  6129  nnsucsssuc  6253  nnaordex  6284  diffifi  6608  fidcenumlemrk  6661  fidcenumlemr  6662  prarloclemup  7052  genpcdl  7076  genpcuu  7077  negf1o  7858  recexap  8120  zaddcllemneg  8787  zdiv  8832  uzaddcl  9072  fz0fzelfz0  9534  fz0fzdiffz0  9537  elfzmlbp  9539  difelfzle  9541  fzo1fzo0n0  9590  ssfzo12bi  9632  exfzdc  9647  modfzo0difsn  9798  frecuzrdgg  9819  iseqvalt  9869  seq3val  9870  exp3vallem  9952  expcllem  9962  expap0  9981  mulexp  9990  cjexp  10323  absexp  10508  fimaxre2  10654  isummo  10769  fsum2d  10825  modfsummod  10848  binom  10874  efexp  10968  demoivreALT  11059  divconjdvds  11124  addmodlteqALT  11134  divalglemeunn  11195  divalglemeuneg  11197  zsupcllemstep  11215  bezoutlemstep  11260  bezoutlemmain  11261  dfgcd2  11277  pw2dvdslemn  11417  nninfalllemn  11853  nninfalllem1  11854  nninfsellemdc  11857  nninfsellemqall  11862
  Copyright terms: Public domain W3C validator