Theorem expdimp 439

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

Hypothesis

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

Assertion

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

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.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  2924  ralcom2  2994  reu6  3261  ssexnelpss  3860  wereu2  4848  ordtr3  5485  oneqmini  5491  fun11iun  6765  poxp  6917  suppssr  6955  smoel  7085  omabs  7354  omsmo  7361  iiner  7441  fodomr  7727  fisseneq  7787  suplub2  7979  supnub  7980  infglb  8010  infnlb  8012  inf3lem6  8142  cfcoflem  8704  coftr  8705  zorn2lem7  8934  alephreg  9009  inar1  9202  gruen  9239  letr  9729  lbzbi  11254  xrletr  11457  xmullem  11552  supxrun  11603  ssfzoulel  12006  ssfzo12bi  12007  hashbnd  12522  fi1uzind  12648  brfi1indALT  12651  cau3lem  13411  summo  13776  mertenslem2  13934  prodmolem2  13982  alzdvds  14348  nn0seqcvgd  14522  lcmdvds  14566  lcmf  14599  prmn2uzge3  14637  divgcdodd  14646  prmpwdvds  14841  catpropd  15607  pltnle  16205  pltval3  16206  pltletr  16210  tsrlemax  16459  frgpnabllem1  17502  cyggexb  17526  abvn0b  18519  isphld  19213  indistopon  20008  restntr  20190  cnprest  20297  lmss  20306  lmmo  20388  2ndcdisj  20463  txlm  20655  flftg  21003  bndth  21978  iscmet3  22255  bcthlem5  22288  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  ellimc3  22826  lhop1  22958  ulmcaulem  23341  ulmcau  23342  ulmcn  23346  xrlimcnp  23886  ax5seglem4  24954  axcontlem2  24987  axcontlem4  24989  clwlkisclwwlklem2a  25505  rusgrasn  25665  frgrawopreglem5  25768  extwwlkfablem2  25798  gxadd  25995  gxmul  25998  nmcvcn  26323  htthlem  26562  atcvat3i  28041  sumdmdlem2  28064  ifeqeqx  28154  bnj23  29526  bnj849  29738  funbreq  30412  sltasym  30560  cgrdegen  30770  lineext  30842  btwnconn1lem7  30859  btwnconn1lem14  30866  waj-ax  31073  lukshef-ax2  31074  relowlssretop  31724  finxpreclem6  31746  fin2solem  31889  poimirlem2  31900  poimirlem18  31916  poimirlem21  31919  poimirlem26  31924  poimirlem27  31925  poimirlem31  31929  unirep  31997  seqpo  32034  ssbnd  32078  intidl  32220  prnc  32258  prtlem15  32409  lshpkrlem6  32644  atlatmstc  32848  cvrat3  32970  ps-2  33006  2lplnj  33148  paddasslem5  33352  dochkrshp4  34920  isnacs3  35515  pm14.24  36685  rexlim2d  37569  iccpartigtl  38493  icceuelpartlem  38505  rngcinv  39325  rngcinvALTV  39337  ringcinv  39376  ringcinvALTV  39400  lindslinindsimp1  39594  lindslinindsimp2  39600  nno  39672  digexp  39762  aacllem  39884