Theorem expimpd 363

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

Hypothesis

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

Assertion

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

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 254	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  euotd  4288  swopo  4342  reusv3  4496  ralxfrd  4498  rexxfrd  4499  nlimsucg  4603  poirr2  5063  elpreima  5684  fmptco  5731  tposfo2  6334  nnm00  6597  th3qlem1  6705  fiintim  7001  supmoti  7068  infglbti  7100  infnlbti  7101  updjud  7157  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  uzind  9456  ledivge1le  9820  xltnegi  9929  ixxssixx  9996  seqf1oglem1  10630  expnegzap  10684  shftlem  11000  cau3lem  11298  caubnd2  11301  climuni  11477  2clim  11485  summodclem2  11566  summodc  11567  zsumdc  11568  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  dfgcd2  12208  cncongrprm  12352  prmpwdvds  12551  infpnlem1  12555  1arith  12563  isgrpid2  13244  dvdsrd  13728  dvdsrtr  13735  dvdsrmul1  13736  unitgrp  13750  domnmuln0  13907  eltg3  14401  tgidm  14418  tgrest  14513  tgcn  14552  lmtopcnp  14594  txbasval  14611  txcnp  14615  bldisj  14745  xblm  14761  blssps  14771  blss  14772  blssexps  14773  blssex  14774  metcnp3  14855  mpomulcn  14910  2lgslem3  15450  2sqlem6  15469  2sqlem7  15470  bj-findis  15733