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  4283  swopo  4337  reusv3  4491  ralxfrd  4493  rexxfrd  4494  nlimsucg  4598  poirr2  5058  elpreima  5677  fmptco  5724  tposfo2  6320  nnm00  6583  th3qlem1  6691  fiintim  6985  supmoti  7052  infglbti  7084  infnlbti  7085  updjud  7141  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  uzind  9428  ledivge1le  9792  xltnegi  9901  ixxssixx  9968  seqf1oglem1  10590  expnegzap  10644  shftlem  10960  cau3lem  11258  caubnd2  11261  climuni  11436  2clim  11444  summodclem2  11525  summodc  11526  zsumdc  11527  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  dfgcd2  12151  cncongrprm  12295  prmpwdvds  12493  infpnlem1  12497  1arith  12505  isgrpid2  13112  dvdsrd  13590  dvdsrtr  13597  dvdsrmul1  13598  unitgrp  13612  domnmuln0  13769  eltg3  14225  tgidm  14242  tgrest  14337  tgcn  14376  lmtopcnp  14418  txbasval  14435  txcnp  14439  bldisj  14569  xblm  14585  blssps  14595  blss  14596  blssexps  14597  blssex  14598  metcnp3  14679  2sqlem6  15207  2sqlem7  15208  bj-findis  15471