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

Theorem expimpd 363
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expimpd.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
expimpd  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 115 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 254 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-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  euotd  4250  swopo  4302  reusv3  4456  ralxfrd  4458  rexxfrd  4459  nlimsucg  4561  poirr2  5016  elpreima  5630  fmptco  5677  tposfo2  6261  nnm00  6524  th3qlem1  6630  fiintim  6921  supmoti  6985  infglbti  7017  infnlbti  7018  updjud  7074  recexprlemss1l  7612  recexprlemss1u  7613  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  caucvgprlemladdrl  7655  uzind  9340  ledivge1le  9700  xltnegi  9809  ixxssixx  9876  expnegzap  10527  shftlem  10796  cau3lem  11094  caubnd2  11097  climuni  11272  2clim  11280  summodclem2  11361  summodc  11362  zsumdc  11363  fsumf1o  11369  fisumss  11371  fsumcl2lem  11377  fsumadd  11385  fsummulc2  11427  prodmodclem2  11556  prodmodc  11557  zproddc  11558  fprodf1o  11567  fprodssdc  11569  fprodmul  11570  dfgcd2  11985  cncongrprm  12127  prmpwdvds  12323  infpnlem1  12327  1arith  12335  isgrpid2  12790  dvdsrd  13075  dvdsrtr  13082  dvdsrmul1  13083  unitgrp  13097  eltg3  13190  tgidm  13207  tgrest  13302  tgcn  13341  lmtopcnp  13383  txbasval  13400  txcnp  13404  bldisj  13534  xblm  13550  blssps  13560  blss  13561  blssexps  13562  blssex  13563  metcnp3  13644  2sqlem6  14089  2sqlem7  14090  bj-findis  14353
  Copyright terms: Public domain W3C validator