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  4376  swopo  4432  reusv3  4586  ralxfrd  4588  rexxfrd  4589  nlimsucg  4693  poirr2  5160  elpreima  5802  fmptco  5848  suppssdc  6473  tposfo2  6511  nnm00  6776  th3qlem1  6884  fiintim  7204  supmoti  7297  infglbti  7329  infnlbti  7330  updjud  7386  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  uzind  9707  ledivge1le  10077  xltnegi  10187  ixxssixx  10254  seqf1oglem1  10905  expnegzap  10959  ccatrcl1  11327  shftlem  11526  cau3lem  11824  caubnd2  11827  climuni  12003  2clim  12011  summodclem2  12093  summodc  12094  zsumdc  12095  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  dfgcd2  12735  cncongrprm  12879  prmpwdvds  13078  infpnlem1  13082  1arith  13090  isgrpid2  13795  dvdsrd  14339  dvdsrtr  14346  dvdsrmul1  14347  unitgrp  14361  domnmuln0  14520  eltg3  15048  tgidm  15065  tgrest  15160  tgcn  15199  lmtopcnp  15241  txbasval  15258  txcnp  15262  bldisj  15392  xblm  15408  blssps  15418  blss  15419  blssexps  15420  blssex  15421  metcnp3  15502  mpomulcn  15557  2lgslem3  16100  2sqlem6  16119  2sqlem7  16120  uspgr2wlkeq  16486  wlklenvclwlk  16494  clwwlkccatlem  16521  clwwlknonel  16553  bj-findis  16875