Theorem expdimp 444

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
expd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expdimp	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		expd.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 443	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 436	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190  df-an 378

This theorem is referenced by:  rexlimdvv  2877  ralcom2  2941  reu6  3215  ssexnelpss  3532  wereu2  4836  ordtr3  5475  oneqmini  5481  fun11iun  6772  poxp  6927  suppssr  6965  smoel  7097  omabs  7366  omsmo  7373  iiner  7453  fodomr  7741  fisseneq  7801  suplub2  7993  supnub  7994  infglb  8024  infnlb  8026  inf3lem6  8156  cfcoflem  8720  coftr  8721  zorn2lem7  8950  alephreg  9025  inar1  9218  gruen  9255  letr  9745  lbzbi  11275  xrletr  11478  xmullem  11575  supxrun  11626  ssfzoulel  12034  ssfzo12bi  12035  hashbnd  12559  fi1uzind  12691  brfi1indALT  12694  fi1uzindOLD  12697  brfi1indALTOLD  12700  cau3lem  13494  summo  13860  mertenslem2  14018  prodmolem2  14066  alzdvds  14432  nn0seqcvgd  14608  lcmdvds  14652  lcmf  14685  prmn2uzge3  14723  divgcdodd  14732  prmpwdvds  14927  catpropd  15692  pltnle  16290  pltval3  16291  pltletr  16295  tsrlemax  16544  frgpnabllem1  17587  cyggexb  17611  abvn0b  18603  isphld  19298  indistopon  20093  restntr  20275  cnprest  20382  lmss  20391  lmmo  20473  2ndcdisj  20548  txlm  20740  flftg  21089  bndth  22064  iscmet3  22341  bcthlem5  22374  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ellimc3  22913  lhop1  23045  ulmcaulem  23428  ulmcau  23429  ulmcn  23433  xrlimcnp  23973  ax5seglem4  25041  axcontlem2  25074  axcontlem4  25076  clwlkisclwwlklem2a  25592  rusgrasn  25752  frgrawopreglem5  25855  extwwlkfablem2  25885  gxadd  26084  gxmul  26087  nmcvcn  26412  htthlem  26651  atcvat3i  28130  sumdmdlem2  28153  ifeqeqx  28236  bnj23  29596  bnj849  29808  funbreq  30482  sltasym  30632  cgrdegen  30842  lineext  30914  btwnconn1lem7  30931  btwnconn1lem14  30938  waj-ax  31145  lukshef-ax2  31146  relowlssretop  31836  finxpreclem6  31858  fin2solem  31995  poimirlem2  32006  poimirlem18  32022  poimirlem21  32025  poimirlem26  32030  poimirlem27  32031  poimirlem31  32035  unirep  32103  seqpo  32140  ssbnd  32184  intidl  32326  prnc  32364  prtlem15  32511  lshpkrlem6  32752  atlatmstc  32956  cvrat3  33078  ps-2  33114  2lplnj  33256  paddasslem5  33460  dochkrshp4  35028  isnacs3  35623  pm14.24  36853  rexlim2d  37802  iccpartigtl  38882  icceuelpartlem  38894  incistruhgr  39325  nbuhgr  39575  uhgrnbgr0nb  39586  spthdep  39926  rngcinv  40491  rngcinvALTV  40503  ringcinv  40542  ringcinvALTV  40566  lindslinindsimp1  40758  lindslinindsimp2  40764  nno  40836  digexp  40926  aacllem  41046