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  4297  swopo  4351  reusv3  4505  ralxfrd  4507  rexxfrd  4508  nlimsucg  4612  poirr2  5072  elpreima  5693  fmptco  5740  tposfo2  6343  nnm00  6606  th3qlem1  6714  fiintim  7010  supmoti  7077  infglbti  7109  infnlbti  7110  updjud  7166  recexprlemss1l  7730  recexprlemss1u  7731  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  caucvgprlemladdrl  7773  uzind  9466  ledivge1le  9830  xltnegi  9939  ixxssixx  10006  seqf1oglem1  10645  expnegzap  10699  shftlem  11046  cau3lem  11344  caubnd2  11347  climuni  11523  2clim  11531  summodclem2  11612  summodc  11613  zsumdc  11614  fsumf1o  11620  fisumss  11622  fsumcl2lem  11628  fsumadd  11636  fsummulc2  11678  prodmodclem2  11807  prodmodc  11808  zproddc  11809  fprodf1o  11818  fprodssdc  11820  fprodmul  11821  dfgcd2  12254  cncongrprm  12398  prmpwdvds  12597  infpnlem1  12601  1arith  12609  isgrpid2  13290  dvdsrd  13774  dvdsrtr  13781  dvdsrmul1  13782  unitgrp  13796  domnmuln0  13953  eltg3  14447  tgidm  14464  tgrest  14559  tgcn  14598  lmtopcnp  14640  txbasval  14657  txcnp  14661  bldisj  14791  xblm  14807  blssps  14817  blss  14818  blssexps  14819  blssex  14820  metcnp3  14901  mpomulcn  14956  2lgslem3  15496  2sqlem6  15515  2sqlem7  15516  bj-findis  15779