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  4397  swopo  4453  reusv3  4608  ralxfrd  4610  rexxfrd  4611  nlimsucg  4715  poirr2  5183  elpreima  5831  fmptco  5877  suppssdc  6504  tposfo2  6543  nnm00  6808  th3qlem1  6916  fiintim  7244  supmoti  7339  infglbti  7371  infnlbti  7372  updjud  7428  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  uzind  9767  ledivge1le  10143  xltnegi  10253  ixxssixx  10320  seqf1oglem1  10976  expnegzap  11030  ccatrcl1  11403  shftlem  11602  cau3lem  11902  caubnd2  11905  climuni  12083  2clim  12091  summodclem2  12173  summodc  12174  zsumdc  12175  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  dfgcd2  12815  cncongrprm  12960  prmpwdvds  13162  infpnlem1  13166  1arith  13174  prmlem0  13248  isgrpid2  13903  dvdsrd  14509  dvdsrtr  14516  dvdsrmul1  14517  unitgrp  14531  domnmuln0  14690  eltg3  15300  tgidm  15317  tgrest  15412  tgcn  15451  lmtopcnp  15493  txbasval  15510  txcnp  15514  bldisj  15644  xblm  15660  blssps  15670  blss  15671  blssexps  15672  blssex  15673  metcnp3  15754  mpomulcn  15809  rpcxpmul2z  16165  2lgslem3  16442  2sqlem6  16461  2sqlem7  16462  uspgr2wlkeq  16828  wlklenvclwlk  16836  clwwlkccatlem  16863  clwwlknonel  16895  bj-findis  17227