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  4345  swopo  4401  reusv3  4555  ralxfrd  4557  rexxfrd  4558  nlimsucg  4662  poirr2  5127  elpreima  5762  fmptco  5809  tposfo2  6428  nnm00  6693  th3qlem1  6801  fiintim  7116  supmoti  7183  infglbti  7215  infnlbti  7216  updjud  7272  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  uzind  9581  ledivge1le  9951  xltnegi  10060  ixxssixx  10127  seqf1oglem1  10771  expnegzap  10825  ccatrcl1  11181  shftlem  11367  cau3lem  11665  caubnd2  11668  climuni  11844  2clim  11852  summodclem2  11933  summodc  11934  zsumdc  11935  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  dfgcd2  12575  cncongrprm  12719  prmpwdvds  12918  infpnlem1  12922  1arith  12930  isgrpid2  13613  dvdsrd  14098  dvdsrtr  14105  dvdsrmul1  14106  unitgrp  14120  domnmuln0  14277  eltg3  14771  tgidm  14788  tgrest  14883  tgcn  14922  lmtopcnp  14964  txbasval  14981  txcnp  14985  bldisj  15115  xblm  15131  blssps  15141  blss  15142  blssexps  15143  blssex  15144  metcnp3  15225  mpomulcn  15280  2lgslem3  15820  2sqlem6  15839  2sqlem7  15840  uspgr2wlkeq  16162  wlklenvclwlk  16170  clwwlkccatlem  16195  clwwlknonel  16227  bj-findis  16510