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  4390  swopo  4446  reusv3  4601  ralxfrd  4603  rexxfrd  4604  nlimsucg  4708  poirr2  5175  elpreima  5819  fmptco  5865  suppssdc  6490  tposfo2  6528  nnm00  6793  th3qlem1  6901  fiintim  7228  supmoti  7323  infglbti  7355  infnlbti  7356  updjud  7412  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  uzind  9736  ledivge1le  10106  xltnegi  10216  ixxssixx  10283  seqf1oglem1  10934  expnegzap  10988  ccatrcl1  11360  shftlem  11559  cau3lem  11858  caubnd2  11861  climuni  12037  2clim  12045  summodclem2  12127  summodc  12128  zsumdc  12129  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  dfgcd2  12769  cncongrprm  12913  prmpwdvds  13112  infpnlem1  13116  1arith  13124  isgrpid2  13822  dvdsrd  14374  dvdsrtr  14381  dvdsrmul1  14382  unitgrp  14396  domnmuln0  14555  eltg3  15081  tgidm  15098  tgrest  15193  tgcn  15232  lmtopcnp  15274  txbasval  15291  txcnp  15295  bldisj  15425  xblm  15441  blssps  15451  blss  15452  blssexps  15453  blssex  15454  metcnp3  15535  mpomulcn  15590  2lgslem3  16134  2sqlem6  16153  2sqlem7  16154  uspgr2wlkeq  16520  wlklenvclwlk  16528  clwwlkccatlem  16555  clwwlknonel  16587  bj-findis  16919