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

Theorem exp31 359
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 114 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32ex 114 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  exp41  365  exp42  366  expl  373  exbiri  377  anasss  394  an31s  542  con4biddc  825  3impa  1159  exp516  1188  rexlimdva2  2527  r19.29af2  2547  disjiun  3892  mpteqb  5477  dffo3  5533  fconstfvm  5604  fliftfun  5663  tfrlem1  6171  tfrlem9  6182  tfr1onlemaccex  6211  tfrcllemaccex  6224  tfrcl  6227  nnsucsssuc  6354  nnaordex  6389  diffifi  6754  fidcenumlemrk  6808  fidcenumlemr  6809  prarloclemup  7267  genpcdl  7291  genpcuu  7292  negf1o  8108  recexap  8374  zaddcllemneg  9044  zdiv  9090  uzaddcl  9330  fz0fzelfz0  9844  fz0fzdiffz0  9847  elfzmlbp  9849  difelfzle  9851  fzo1fzo0n0  9900  ssfzo12bi  9942  exfzdc  9957  modfzo0difsn  10108  frecuzrdgg  10129  seq3val  10171  seqvalcd  10172  exp3vallem  10234  expcllem  10244  expap0  10263  mulexp  10272  cjexp  10605  absexp  10791  fimaxre2  10938  summodc  11092  fsum2d  11144  modfsummod  11167  binom  11193  efexp  11287  demoivreALT  11378  divconjdvds  11443  addmodlteqALT  11453  divalglemeunn  11514  divalglemeuneg  11516  zsupcllemstep  11534  bezoutlemstep  11581  bezoutlemmain  11582  dfgcd2  11598  pw2dvdslemn  11738  topbas  12131  cnplimclemr  12681  limccnp2lem  12688  nninfalllemn  13004  nninfalllem1  13005  nninfsellemdc  13008  nninfsellemqall  13013  isomninnlem  13027
  Copyright terms: Public domain W3C validator