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  4353  swopo  4409  reusv3  4563  ralxfrd  4565  rexxfrd  4566  nlimsucg  4670  poirr2  5136  elpreima  5775  fmptco  5821  suppssdc  6438  tposfo2  6476  nnm00  6741  th3qlem1  6849  fiintim  7166  supmoti  7235  infglbti  7267  infnlbti  7268  updjud  7324  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  uzind  9635  ledivge1le  10005  xltnegi  10114  ixxssixx  10181  seqf1oglem1  10827  expnegzap  10881  ccatrcl1  11240  shftlem  11439  cau3lem  11737  caubnd2  11740  climuni  11916  2clim  11924  summodclem2  12006  summodc  12007  zsumdc  12008  fsumf1o  12014  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  dfgcd2  12648  cncongrprm  12792  prmpwdvds  12991  infpnlem1  12995  1arith  13003  isgrpid2  13686  dvdsrd  14172  dvdsrtr  14179  dvdsrmul1  14180  unitgrp  14194  domnmuln0  14352  eltg3  14851  tgidm  14868  tgrest  14963  tgcn  15002  lmtopcnp  15044  txbasval  15061  txcnp  15065  bldisj  15195  xblm  15211  blssps  15221  blss  15222  blssexps  15223  blssex  15224  metcnp3  15305  mpomulcn  15360  2lgslem3  15903  2sqlem6  15922  2sqlem7  15923  uspgr2wlkeq  16289  wlklenvclwlk  16297  clwwlkccatlem  16324  clwwlknonel  16356  bj-findis  16678