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  4395  swopo  4451  reusv3  4606  ralxfrd  4608  rexxfrd  4609  nlimsucg  4713  poirr2  5180  elpreima  5828  fmptco  5874  suppssdc  6500  tposfo2  6538  nnm00  6803  th3qlem1  6911  fiintim  7238  supmoti  7334  infglbti  7366  infnlbti  7367  updjud  7423  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  uzind  9762  ledivge1le  10138  xltnegi  10248  ixxssixx  10315  seqf1oglem1  10971  expnegzap  11025  ccatrcl1  11398  shftlem  11597  cau3lem  11897  caubnd2  11900  climuni  12078  2clim  12086  summodclem2  12168  summodc  12169  zsumdc  12170  fsumf1o  12176  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodf1o  12374  fprodssdc  12376  fprodmul  12377  dfgcd2  12810  cncongrprm  12955  prmpwdvds  13157  infpnlem1  13161  1arith  13169  prmlem0  13243  isgrpid2  13898  dvdsrd  14485  dvdsrtr  14492  dvdsrmul1  14493  unitgrp  14507  domnmuln0  14666  eltg3  15249  tgidm  15266  tgrest  15361  tgcn  15400  lmtopcnp  15442  txbasval  15459  txcnp  15463  bldisj  15593  xblm  15609  blssps  15619  blss  15620  blssexps  15621  blssex  15622  metcnp3  15703  mpomulcn  15758  2lgslem3  16386  2sqlem6  16405  2sqlem7  16406  uspgr2wlkeq  16772  wlklenvclwlk  16780  clwwlkccatlem  16807  clwwlknonel  16839  bj-findis  17171