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  2852  ralcom2  2890  reu6  3153  wereu2  4722  ordtr3  4769  oneqmini  4775  suppssrOLD  5842  fun11iun  6542  poxp  6689  suppssr  6725  smoel  6826  omabs  7091  omsmo  7098  iiner  7177  fodomr  7467  fisseneq  7529  suplub2  7716  supnub  7717  inf3lem6  7844  cfcoflem  8446  coftr  8447  zorn2lem7  8676  alephreg  8751  inar1  8947  gruen  8984  letr  9473  lbzbi  10948  xrletr  11137  xmullem  11232  supxrun  11283  ssfzoulel  11626  ssfzo12bi  11627  hashbnd  12114  brfi1uzind  12224  cau3lem  12847  summo  13199  mertenslem2  13350  alzdvds  13588  nn0seqcvgd  13750  divgcdodd  13810  prmpwdvds  13970  catpropd  14653  pltnle  15141  pltval3  15142  pltletr  15146  tsrlemax  15395  frgpnabllem1  16356  cyggexb  16380  abvn0b  17379  isphld  18088  indistopon  18610  restntr  18791  cnprest  18898  lmss  18907  lmmo  18989  2ndcdisj  19065  txlm  19226  flftg  19574  bndth  20535  iscmet3  20809  bcthlem5  20844  ovolicc2lem4  21008  ellimc3  21359  lhop1  21491  ulmcaulem  21864  ulmcau  21865  ulmcn  21869  xrlimcnp  22367  ax5seglem4  23183  axcontlem2  23216  axcontlem4  23218  gxadd  23767  gxmul  23770  nmcvcn  24095  htthlem  24324  atcvat3i  25805  sumdmdlem2  25828  ifeqeqx  25907  prodmolem2  27453  funbreq  27587  sltasym  27818  cgrdegen  28040  lineext  28112  btwnconn1lem7  28129  btwnconn1lem14  28136  waj-ax  28265  lukshef-ax2  28266  fin2solem  28420  unirep  28611  seqpo  28648  ssbnd  28692  intidl  28834  prnc  28872  prtlem15  29025  isnacs3  29051  pm14.24  29691  prmn2uzge3  30254  clwlkisclwwlklem2a  30452  rusgrasn  30562  frgrawopreglem5  30646  extwwlkfablem2  30676  lindslinindsimp1  30996  lindslinindsimp2  31002  bnj23  31712  bnj849  31923  lshpkrlem6  32765  atlatmstc  32969  cvrat3  33091  ps-2  33127  2lplnj  33269  paddasslem5  33473  dochkrshp4  35039