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  7719  recexprlemss1u  7720  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  uzind  9454  ledivge1le  9818  xltnegi  9927  ixxssixx  9994  seqf1oglem1  10628  expnegzap  10682  shftlem  10998  cau3lem  11296  caubnd2  11299  climuni  11475  2clim  11483  summodclem2  11564  summodc  11565  zsumdc  11566  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  dfgcd2  12206  cncongrprm  12350  prmpwdvds  12549  infpnlem1  12553  1arith  12561  isgrpid2  13242  dvdsrd  13726  dvdsrtr  13733  dvdsrmul1  13734  unitgrp  13748  domnmuln0  13905  eltg3  14377  tgidm  14394  tgrest  14489  tgcn  14528  lmtopcnp  14570  txbasval  14587  txcnp  14591  bldisj  14721  xblm  14737  blssps  14747  blss  14748  blssexps  14749  blssex  14750  metcnp3  14831  mpomulcn  14886  2lgslem3  15426  2sqlem6  15445  2sqlem7  15446  bj-findis  15709