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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  euotd  4395  swopo  4451  reusv3  4606  ralxfrd  4608  rexxfrd  4609  nlimsucg  4713  poirr2  5180  elpreima  5828  fmptco  5874  suppssdc  6500  tposfo2  6538  nnm00  6803  th3qlem1  6911  fiintim  7238  supmoti  7333  infglbti  7365  infnlbti  7366  updjud  7422  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  uzind  9761  ledivge1le  10137  xltnegi  10247  ixxssixx  10314  seqf1oglem1  10969  expnegzap  11023  ccatrcl1  11396  shftlem  11595  cau3lem  11895  caubnd2  11898  climuni  12075  2clim  12083  summodclem2  12165  summodc  12166  zsumdc  12167  fsumf1o  12173  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodf1o  12371  fprodssdc  12373  fprodmul  12374  dfgcd2  12807  cncongrprm  12952  prmpwdvds  13154  infpnlem1  13158  1arith  13166  prmlem0  13240  isgrpid2  13894  dvdsrd  14450  dvdsrtr  14457  dvdsrmul1  14458  unitgrp  14472  domnmuln0  14631  eltg3  15207  tgidm  15224  tgrest  15319  tgcn  15358  lmtopcnp  15400  txbasval  15417  txcnp  15421  bldisj  15551  xblm  15567  blssps  15577  blss  15578  blssexps  15579  blssex  15580  metcnp3  15661  mpomulcn  15716  2lgslem3  16318  2sqlem6  16337  2sqlem7  16338  uspgr2wlkeq  16704  wlklenvclwlk  16712  clwwlkccatlem  16739  clwwlknonel  16771  bj-findis  17103