Theorem expdimp 439

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 438	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 431	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  rexlimdvv  2885  ralcom2  2955  reu6  3227  ssexnelpss  3831  wereu2  4831  ordtr3  5468  oneqmini  5474  fun11iun  6753  poxp  6908  suppssr  6946  smoel  7079  omabs  7348  omsmo  7355  iiner  7435  fodomr  7723  fisseneq  7783  suplub2  7975  supnub  7976  infglb  8006  infnlb  8008  inf3lem6  8138  cfcoflem  8702  coftr  8703  zorn2lem7  8932  alephreg  9007  inar1  9200  gruen  9237  letr  9727  lbzbi  11252  xrletr  11455  xmullem  11550  supxrun  11601  ssfzoulel  12005  ssfzo12bi  12006  hashbnd  12521  fi1uzind  12650  brfi1indALT  12653  cau3lem  13417  summo  13783  mertenslem2  13941  prodmolem2  13989  alzdvds  14355  nn0seqcvgd  14529  lcmdvds  14573  lcmf  14606  prmn2uzge3  14644  divgcdodd  14653  prmpwdvds  14848  catpropd  15614  pltnle  16212  pltval3  16213  pltletr  16217  tsrlemax  16466  frgpnabllem1  17509  cyggexb  17533  abvn0b  18526  isphld  19221  indistopon  20016  restntr  20198  cnprest  20305  lmss  20314  lmmo  20396  2ndcdisj  20471  txlm  20663  flftg  21011  bndth  21986  iscmet3  22263  bcthlem5  22296  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ellimc3  22834  lhop1  22966  ulmcaulem  23349  ulmcau  23350  ulmcn  23354  xrlimcnp  23894  ax5seglem4  24962  axcontlem2  24995  axcontlem4  24997  clwlkisclwwlklem2a  25513  rusgrasn  25673  frgrawopreglem5  25776  extwwlkfablem2  25806  gxadd  26003  gxmul  26006  nmcvcn  26331  htthlem  26570  atcvat3i  28049  sumdmdlem2  28072  ifeqeqx  28158  bnj23  29524  bnj849  29736  funbreq  30411  sltasym  30561  cgrdegen  30771  lineext  30843  btwnconn1lem7  30860  btwnconn1lem14  30867  waj-ax  31074  lukshef-ax2  31075  relowlssretop  31766  finxpreclem6  31788  fin2solem  31931  poimirlem2  31942  poimirlem18  31958  poimirlem21  31961  poimirlem26  31966  poimirlem27  31967  poimirlem31  31971  unirep  32039  seqpo  32076  ssbnd  32120  intidl  32262  prnc  32300  prtlem15  32447  lshpkrlem6  32681  atlatmstc  32885  cvrat3  33007  ps-2  33043  2lplnj  33185  paddasslem5  33389  dochkrshp4  34957  isnacs3  35552  pm14.24  36783  rexlim2d  37705  iccpartigtl  38737  icceuelpartlem  38749  incistruhgr  39171  nbuhgr  39411  uhgrnbgr0nb  39422  rngcinv  40036  rngcinvALTV  40048  ringcinv  40087  ringcinvALTV  40111  lindslinindsimp1  40303  lindslinindsimp2  40309  nno  40381  digexp  40471  aacllem  40593