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  6433  nnm00  6698  th3qlem1  6806  fiintim  7123  supmoti  7192  infglbti  7224  infnlbti  7225  updjud  7281  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  uzind  9591  ledivge1le  9961  xltnegi  10070  ixxssixx  10137  seqf1oglem1  10782  expnegzap  10836  ccatrcl1  11195  shftlem  11394  cau3lem  11692  caubnd2  11695  climuni  11871  2clim  11879  summodclem2  11961  summodc  11962  zsumdc  11963  fsumf1o  11969  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodf1o  12167  fprodssdc  12169  fprodmul  12170  dfgcd2  12603  cncongrprm  12747  prmpwdvds  12946  infpnlem1  12950  1arith  12958  isgrpid2  13641  dvdsrd  14127  dvdsrtr  14134  dvdsrmul1  14135  unitgrp  14149  domnmuln0  14306  eltg3  14800  tgidm  14817  tgrest  14912  tgcn  14951  lmtopcnp  14993  txbasval  15010  txcnp  15014  bldisj  15144  xblm  15160  blssps  15170  blss  15171  blssexps  15172  blssex  15173  metcnp3  15254  mpomulcn  15309  2lgslem3  15849  2sqlem6  15868  2sqlem7  15869  uspgr2wlkeq  16235  wlklenvclwlk  16243  clwwlkccatlem  16270  clwwlknonel  16302  bj-findis  16625