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  7333  infglbti  7365  infnlbti  7366  updjud  7422  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  uzind  9757  ledivge1le  10127  xltnegi  10237  ixxssixx  10304  seqf1oglem1  10956  expnegzap  11010  ccatrcl1  11382  shftlem  11581  cau3lem  11880  caubnd2  11883  climuni  12059  2clim  12067  summodclem2  12149  summodc  12150  zsumdc  12151  fsumf1o  12157  fisumss  12159  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodf1o  12355  fprodssdc  12357  fprodmul  12358  dfgcd2  12791  cncongrprm  12935  prmpwdvds  13134  infpnlem1  13138  1arith  13146  isgrpid2  13845  dvdsrd  14401  dvdsrtr  14408  dvdsrmul1  14409  unitgrp  14423  domnmuln0  14582  eltg3  15158  tgidm  15175  tgrest  15270  tgcn  15309  lmtopcnp  15351  txbasval  15368  txcnp  15372  bldisj  15502  xblm  15518  blssps  15528  blss  15529  blssexps  15530  blssex  15531  metcnp3  15612  mpomulcn  15667  2lgslem3  16220  2sqlem6  16239  2sqlem7  16240  uspgr2wlkeq  16606  wlklenvclwlk  16614  clwwlkccatlem  16641  clwwlknonel  16673  bj-findis  17005