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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  euotd  4397  swopo  4453  reusv3  4608  ralxfrd  4610  rexxfrd  4611  nlimsucg  4715  poirr2  5183  elpreima  5831  fmptco  5877  suppssdc  6504  tposfo2  6542  nnm00  6807  th3qlem1  6915  fiintim  7242  supmoti  7339  infglbti  7371  infnlbti  7372  updjud  7428  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  uzind  9768  ledivge1le  10144  xltnegi  10254  ixxssixx  10321  seqf1oglem1  10977  expnegzap  11031  ccatrcl1  11404  shftlem  11603  cau3lem  11903  caubnd2  11906  climuni  12084  2clim  12092  summodclem2  12174  summodc  12175  zsumdc  12176  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  dfgcd2  12816  cncongrprm  12961  prmpwdvds  13163  infpnlem1  13167  1arith  13175  prmlem0  13249  isgrpid2  13904  dvdsrd  14510  dvdsrtr  14517  dvdsrmul1  14518  unitgrp  14532  domnmuln0  14691  eltg3  15283  tgidm  15300  tgrest  15395  tgcn  15434  lmtopcnp  15476  txbasval  15493  txcnp  15497  bldisj  15627  xblm  15643  blssps  15653  blss  15654  blssexps  15655  blssex  15656  metcnp3  15737  mpomulcn  15792  rpcxpmul2z  16148  2lgslem3  16425  2sqlem6  16444  2sqlem7  16445  uspgr2wlkeq  16811  wlklenvclwlk  16819  clwwlkccatlem  16846  clwwlknonel  16878  bj-findis  17210