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  4307  swopo  4361  reusv3  4515  ralxfrd  4517  rexxfrd  4518  nlimsucg  4622  poirr2  5084  elpreima  5712  fmptco  5759  tposfo2  6366  nnm00  6629  th3qlem1  6737  fiintim  7043  supmoti  7110  infglbti  7142  infnlbti  7143  updjud  7199  recexprlemss1l  7768  recexprlemss1u  7769  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  uzind  9504  ledivge1le  9868  xltnegi  9977  ixxssixx  10044  seqf1oglem1  10686  expnegzap  10740  shftlem  11202  cau3lem  11500  caubnd2  11503  climuni  11679  2clim  11687  summodclem2  11768  summodc  11769  zsumdc  11770  fsumf1o  11776  fisumss  11778  fsumcl2lem  11784  fsumadd  11792  fsummulc2  11834  prodmodclem2  11963  prodmodc  11964  zproddc  11965  fprodf1o  11974  fprodssdc  11976  fprodmul  11977  dfgcd2  12410  cncongrprm  12554  prmpwdvds  12753  infpnlem1  12757  1arith  12765  isgrpid2  13447  dvdsrd  13931  dvdsrtr  13938  dvdsrmul1  13939  unitgrp  13953  domnmuln0  14110  eltg3  14604  tgidm  14621  tgrest  14716  tgcn  14755  lmtopcnp  14797  txbasval  14814  txcnp  14818  bldisj  14948  xblm  14964  blssps  14974  blss  14975  blssexps  14976  blssex  14977  metcnp3  15058  mpomulcn  15113  2lgslem3  15653  2sqlem6  15672  2sqlem7  15673  bj-findis  16053