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  4287  swopo  4341  reusv3  4495  ralxfrd  4497  rexxfrd  4498  nlimsucg  4602  poirr2  5062  elpreima  5681  fmptco  5728  tposfo2  6325  nnm00  6588  th3qlem1  6696  fiintim  6992  supmoti  7059  infglbti  7091  infnlbti  7092  updjud  7148  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  uzind  9437  ledivge1le  9801  xltnegi  9910  ixxssixx  9977  seqf1oglem1  10611  expnegzap  10665  shftlem  10981  cau3lem  11279  caubnd2  11282  climuni  11458  2clim  11466  summodclem2  11547  summodc  11548  zsumdc  11549  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  dfgcd2  12181  cncongrprm  12325  prmpwdvds  12524  infpnlem1  12528  1arith  12536  isgrpid2  13172  dvdsrd  13650  dvdsrtr  13657  dvdsrmul1  13658  unitgrp  13672  domnmuln0  13829  eltg3  14293  tgidm  14310  tgrest  14405  tgcn  14444  lmtopcnp  14486  txbasval  14503  txcnp  14507  bldisj  14637  xblm  14653  blssps  14663  blss  14664  blssexps  14665  blssex  14666  metcnp3  14747  mpomulcn  14802  2lgslem3  15342  2sqlem6  15361  2sqlem7  15362  bj-findis  15625