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  4252  swopo  4304  reusv3  4458  ralxfrd  4460  rexxfrd  4461  nlimsucg  4563  poirr2  5018  elpreima  5632  fmptco  5679  tposfo2  6263  nnm00  6526  th3qlem1  6632  fiintim  6923  supmoti  6987  infglbti  7019  infnlbti  7020  updjud  7076  recexprlemss1l  7629  recexprlemss1u  7630  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  caucvgprlemladdrl  7672  uzind  9358  ledivge1le  9720  xltnegi  9829  ixxssixx  9896  expnegzap  10547  shftlem  10816  cau3lem  11114  caubnd2  11117  climuni  11292  2clim  11300  summodclem2  11381  summodc  11382  zsumdc  11383  fsumf1o  11389  fisumss  11391  fsumcl2lem  11397  fsumadd  11405  fsummulc2  11447  prodmodclem2  11576  prodmodc  11577  zproddc  11578  fprodf1o  11587  fprodssdc  11589  fprodmul  11590  dfgcd2  12005  cncongrprm  12147  prmpwdvds  12343  infpnlem1  12347  1arith  12355  isgrpid2  12841  dvdsrd  13162  dvdsrtr  13169  dvdsrmul1  13170  unitgrp  13184  eltg3  13339  tgidm  13356  tgrest  13451  tgcn  13490  lmtopcnp  13532  txbasval  13549  txcnp  13553  bldisj  13683  xblm  13699  blssps  13709  blss  13710  blssexps  13711  blssex  13712  metcnp3  13793  2sqlem6  14238  2sqlem7  14239  bj-findis  14502