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  4347  swopo  4403  reusv3  4557  ralxfrd  4559  rexxfrd  4560  nlimsucg  4664  poirr2  5129  elpreima  5766  fmptco  5813  tposfo2  6432  nnm00  6697  th3qlem1  6805  fiintim  7122  supmoti  7191  infglbti  7223  infnlbti  7224  updjud  7280  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  uzind  9590  ledivge1le  9960  xltnegi  10069  ixxssixx  10136  seqf1oglem1  10780  expnegzap  10834  ccatrcl1  11190  shftlem  11376  cau3lem  11674  caubnd2  11677  climuni  11853  2clim  11861  summodclem2  11942  summodc  11943  zsumdc  11944  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  dfgcd2  12584  cncongrprm  12728  prmpwdvds  12927  infpnlem1  12931  1arith  12939  isgrpid2  13622  dvdsrd  14107  dvdsrtr  14114  dvdsrmul1  14115  unitgrp  14129  domnmuln0  14286  eltg3  14780  tgidm  14797  tgrest  14892  tgcn  14931  lmtopcnp  14973  txbasval  14990  txcnp  14994  bldisj  15124  xblm  15140  blssps  15150  blss  15151  blssexps  15152  blssex  15153  metcnp3  15234  mpomulcn  15289  2lgslem3  15829  2sqlem6  15848  2sqlem7  15849  uspgr2wlkeq  16215  wlklenvclwlk  16223  clwwlkccatlem  16250  clwwlknonel  16282  bj-findis  16574