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  4255  swopo  4307  reusv3  4461  ralxfrd  4463  rexxfrd  4464  nlimsucg  4566  poirr2  5022  elpreima  5636  fmptco  5683  tposfo2  6268  nnm00  6531  th3qlem1  6637  fiintim  6928  supmoti  6992  infglbti  7024  infnlbti  7025  updjud  7081  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  uzind  9364  ledivge1le  9726  xltnegi  9835  ixxssixx  9902  expnegzap  10554  shftlem  10825  cau3lem  11123  caubnd2  11126  climuni  11301  2clim  11309  summodclem2  11390  summodc  11391  zsumdc  11392  fsumf1o  11398  fisumss  11400  fsumcl2lem  11406  fsumadd  11414  fsummulc2  11456  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodf1o  11596  fprodssdc  11598  fprodmul  11599  dfgcd2  12015  cncongrprm  12157  prmpwdvds  12353  infpnlem1  12357  1arith  12365  isgrpid2  12913  dvdsrd  13263  dvdsrtr  13270  dvdsrmul1  13271  unitgrp  13285  eltg3  13560  tgidm  13577  tgrest  13672  tgcn  13711  lmtopcnp  13753  txbasval  13770  txcnp  13774  bldisj  13904  xblm  13920  blssps  13930  blss  13931  blssexps  13932  blssex  13933  metcnp3  14014  2sqlem6  14470  2sqlem7  14471  bj-findis  14734