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  4298  swopo  4352  reusv3  4506  ralxfrd  4508  rexxfrd  4509  nlimsucg  4613  poirr2  5074  elpreima  5698  fmptco  5745  tposfo2  6352  nnm00  6615  th3qlem1  6723  fiintim  7027  supmoti  7094  infglbti  7126  infnlbti  7127  updjud  7183  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  uzind  9483  ledivge1le  9847  xltnegi  9956  ixxssixx  10023  seqf1oglem1  10662  expnegzap  10716  shftlem  11069  cau3lem  11367  caubnd2  11370  climuni  11546  2clim  11554  summodclem2  11635  summodc  11636  zsumdc  11637  fsumf1o  11643  fisumss  11645  fsumcl2lem  11651  fsumadd  11659  fsummulc2  11701  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodf1o  11841  fprodssdc  11843  fprodmul  11844  dfgcd2  12277  cncongrprm  12421  prmpwdvds  12620  infpnlem1  12624  1arith  12632  isgrpid2  13314  dvdsrd  13798  dvdsrtr  13805  dvdsrmul1  13806  unitgrp  13820  domnmuln0  13977  eltg3  14471  tgidm  14488  tgrest  14583  tgcn  14622  lmtopcnp  14664  txbasval  14681  txcnp  14685  bldisj  14815  xblm  14831  blssps  14841  blss  14842  blssexps  14843  blssex  14844  metcnp3  14925  mpomulcn  14980  2lgslem3  15520  2sqlem6  15539  2sqlem7  15540  bj-findis  15848