Theorem expdimp 437

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  rexlimdvv  2961  ralcom2  3026  reu6  3292  wereu2  4876  ordtr3  4923  oneqmini  4929  suppssrOLD  6013  fun11iun  6741  poxp  6892  suppssr  6928  smoel  7028  omabs  7293  omsmo  7300  iiner  7380  fodomr  7665  fisseneq  7728  suplub2  7917  supnub  7918  inf3lem6  8046  cfcoflem  8648  coftr  8649  zorn2lem7  8878  alephreg  8953  inar1  9149  gruen  9186  letr  9674  lbzbi  11166  xrletr  11357  xmullem  11452  supxrun  11503  ssfzoulel  11870  ssfzo12bi  11871  hashbnd  12375  brfi1uzind  12494  cau3lem  13146  summo  13498  mertenslem2  13653  alzdvds  13891  nn0seqcvgd  14054  prmn2uzge3  14092  divgcdodd  14115  prmpwdvds  14277  catpropd  14961  pltnle  15449  pltval3  15450  pltletr  15454  tsrlemax  15703  frgpnabllem1  16668  cyggexb  16692  abvn0b  17722  isphld  18456  indistopon  19268  restntr  19449  cnprest  19556  lmss  19565  lmmo  19647  2ndcdisj  19723  txlm  19884  flftg  20232  bndth  21193  iscmet3  21467  bcthlem5  21502  ovolicc2lem4  21666  ellimc3  22018  lhop1  22150  ulmcaulem  22523  ulmcau  22524  ulmcn  22528  xrlimcnp  23026  ax5seglem4  23911  axcontlem2  23944  axcontlem4  23946  clwlkisclwwlklem2a  24461  rusgrasn  24621  frgrawopreglem5  24725  extwwlkfablem2  24755  gxadd  24953  gxmul  24956  nmcvcn  25281  htthlem  25510  atcvat3i  26991  sumdmdlem2  27014  ifeqeqx  27093  prodmolem2  28644  funbreq  28778  sltasym  29009  cgrdegen  29231  lineext  29303  btwnconn1lem7  29320  btwnconn1lem14  29327  waj-ax  29456  lukshef-ax2  29457  fin2solem  29616  unirep  29806  seqpo  29843  ssbnd  29887  intidl  30029  prnc  30067  prtlem15  30220  isnacs3  30246  lcmdvds  30814  pm14.24  30917  rexlim2d  31167  lindslinindsimp1  32131  lindslinindsimp2  32137  bnj23  32851  bnj849  33062  lshpkrlem6  33912  atlatmstc  34116  cvrat3  34238  ps-2  34274  2lplnj  34416  paddasslem5  34620  dochkrshp4  36186