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  4284  swopo  4338  reusv3  4492  ralxfrd  4494  rexxfrd  4495  nlimsucg  4599  poirr2  5059  elpreima  5678  fmptco  5725  tposfo2  6322  nnm00  6585  th3qlem1  6693  fiintim  6987  supmoti  7054  infglbti  7086  infnlbti  7087  updjud  7143  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  uzind  9431  ledivge1le  9795  xltnegi  9904  ixxssixx  9971  seqf1oglem1  10593  expnegzap  10647  shftlem  10963  cau3lem  11261  caubnd2  11264  climuni  11439  2clim  11447  summodclem2  11528  summodc  11529  zsumdc  11530  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  dfgcd2  12154  cncongrprm  12298  prmpwdvds  12496  infpnlem1  12500  1arith  12508  isgrpid2  13115  dvdsrd  13593  dvdsrtr  13600  dvdsrmul1  13601  unitgrp  13615  domnmuln0  13772  eltg3  14236  tgidm  14253  tgrest  14348  tgcn  14387  lmtopcnp  14429  txbasval  14446  txcnp  14450  bldisj  14580  xblm  14596  blssps  14606  blss  14607  blssexps  14608  blssex  14609  metcnp3  14690  mpomulcn  14745  2lgslem3  15258  2sqlem6  15277  2sqlem7  15278  bj-findis  15541