Theorem expdimp 453

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  rexlimdvv  3037  ralcom2  3104  ssexnelpss  3720  wereu2  5111  oneqmini  5776  suctr  5808  fun11iun  7126  poxp  7289  suppssr  7326  smoel  7457  omabs  7727  omsmo  7734  iiner  7819  fodomr  8111  fisseneq  8171  suplub2  8367  supnub  8368  infglb  8396  infnlb  8398  inf3lem6  8530  cfcoflem  9094  coftr  9095  zorn2lem7  9324  alephreg  9404  inar1  9597  gruen  9634  letr  10131  lbzbi  11776  xrletr  11989  xmullem  12094  supxrun  12146  ssfzoulel  12562  ssfzo12bi  12563  hashbnd  13123  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  cau3lem  14094  summo  14448  mertenslem2  14617  prodmolem2  14665  alzdvds  15042  nno  15098  nn0seqcvgd  15283  lcmdvds  15321  lcmf  15346  divgcdodd  15422  prmpwdvds  15608  catpropd  16369  pltnle  16966  pltval3  16967  pltletr  16971  tsrlemax  17220  frgpnabllem1  18276  cyggexb  18300  abvn0b  19302  isphld  19999  indistopon  20805  restntr  20986  cnprest  21093  lmss  21102  lmmo  21184  2ndcdisj  21259  txlm  21451  flftg  21800  bndth  22757  iscmet3  23091  bcthlem5  23125  ovolicc2lem4  23288  ellimc3  23643  lhop1  23777  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  xrlimcnp  24695  ax5seglem4  25812  axcontlem2  25845  axcontlem4  25847  incistruhgr  25974  nbuhgr  26239  uhgrnbgr0nb  26250  wwlknp  26734  wwlksnred  26787  clwlkclwwlklem2a  26899  vdgn0frgrv2  27159  nmcvcn  27550  htthlem  27774  atcvat3i  29255  sumdmdlem2  29278  ifeqeqx  29361  bnj23  30784  bnj849  30995  sotr3  31656  funbreq  31668  nosepssdm  31836  cgrdegen  32111  lineext  32183  btwnconn1lem7  32200  btwnconn1lem14  32207  waj-ax  32413  lukshef-ax2  32414  relowlssretop  33211  finxpreclem6  33233  fin2solem  33395  poimirlem2  33411  poimirlem18  33427  poimirlem21  33430  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  unirep  33507  seqpo  33543  ssbnd  33587  intidl  33828  prnc  33866  prtlem15  34160  lshpkrlem6  34402  atlatmstc  34606  cvrat3  34728  ps-2  34764  2lplnj  34906  paddasslem5  35110  dochkrshp4  36678  isnacs3  37273  pm14.24  38633  rexlim2d  39857  iccpartigtl  41359  icceuelpartlem  41371  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  lindslinindsimp1  42246  lindslinindsimp2  42252  digexp  42401  aacllem  42547