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  4341  swopo  4397  reusv3  4551  ralxfrd  4553  rexxfrd  4554  nlimsucg  4658  poirr2  5121  elpreima  5756  fmptco  5803  tposfo2  6419  nnm00  6684  th3qlem1  6792  fiintim  7104  supmoti  7171  infglbti  7203  infnlbti  7204  updjud  7260  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  uzind  9569  ledivge1le  9934  xltnegi  10043  ixxssixx  10110  seqf1oglem1  10753  expnegzap  10807  ccatrcl1  11162  shftlem  11342  cau3lem  11640  caubnd2  11643  climuni  11819  2clim  11827  summodclem2  11908  summodc  11909  zsumdc  11910  fsumf1o  11916  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  dfgcd2  12550  cncongrprm  12694  prmpwdvds  12893  infpnlem1  12897  1arith  12905  isgrpid2  13588  dvdsrd  14073  dvdsrtr  14080  dvdsrmul1  14081  unitgrp  14095  domnmuln0  14252  eltg3  14746  tgidm  14763  tgrest  14858  tgcn  14897  lmtopcnp  14939  txbasval  14956  txcnp  14960  bldisj  15090  xblm  15106  blssps  15116  blss  15117  blssexps  15118  blssex  15119  metcnp3  15200  mpomulcn  15255  2lgslem3  15795  2sqlem6  15814  2sqlem7  15815  uspgr2wlkeq  16106  wlklenvclwlk  16114  clwwlkccatlem  16137  bj-findis  16397