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

Theorem exp31 361
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  367  exp42  368  expl  375  exbiri  379  anasss  396  an31s  544  con4biddc  827  3impa  1161  exp516  1190  rexlimdva2  2529  r19.29af2  2549  disjiun  3894  mpteqb  5479  dffo3  5535  fconstfvm  5606  fliftfun  5665  tfrlem1  6173  tfrlem9  6184  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcl  6229  nnsucsssuc  6356  nnaordex  6391  diffifi  6756  fidcenumlemrk  6810  fidcenumlemr  6811  prarloclemup  7271  genpcdl  7295  genpcuu  7296  negf1o  8112  recexap  8382  zaddcllemneg  9061  zdiv  9107  uzaddcl  9349  fz0fzelfz0  9872  fz0fzdiffz0  9875  elfzmlbp  9877  difelfzle  9879  fzo1fzo0n0  9928  ssfzo12bi  9970  exfzdc  9985  modfzo0difsn  10136  frecuzrdgg  10157  seq3val  10199  seqvalcd  10200  exp3vallem  10262  expcllem  10272  expap0  10291  mulexp  10300  cjexp  10633  absexp  10819  fimaxre2  10966  summodc  11120  fsum2d  11172  modfsummod  11195  binom  11221  efexp  11315  demoivreALT  11407  divconjdvds  11474  addmodlteqALT  11484  divalglemeunn  11545  divalglemeuneg  11547  zsupcllemstep  11565  bezoutlemstep  11612  bezoutlemmain  11613  dfgcd2  11629  pw2dvdslemn  11770  topbas  12163  cnplimclemr  12734  limccnp2lem  12741  nninfalllemn  13129  nninfalllem1  13130  nninfsellemdc  13133  nninfsellemqall  13138  isomninnlem  13152
  Copyright terms: Public domain W3C validator