Theorem impd 254

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
imp3.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
impd	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		imp3.1	. . . 4 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3l 81	. . 3 |- ( ps -> ( ch -> ( ph -> th ) ) )
3	2	imp 124	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
4	3	com12 30	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

This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  690  pm5.6r  928  3expib  1208  sbiedh  1798  equs5  1840  moexexdc  2122  rsp2  2540  moi  2935  reu6  2941  sbciegft  3008  prel12  3789  opthpr  3790  invdisj  4015  sowlin  4341  reusv1  4479  relop  4798  elres  4964  iss  4974  funssres  5280  fv3  5560  funfvima  5772  poxp  6261  tfri3  6396  nndi  6515  nnmass  6516  nnmordi  6545  nnmord  6546  eroveu  6656  fiintim  6961  suplubti  7033  addnq0mo  7481  mulnq0mo  7482  prcdnql  7518  prcunqu  7519  prnmaxl  7522  prnminu  7523  genprndl  7555  genprndu  7556  distrlem1prl  7616  distrlem1pru  7617  distrlem5prl  7620  distrlem5pru  7621  recexprlemss1l  7669  recexprlemss1u  7670  addsrmo  7777  mulsrmo  7778  mulgt0sr  7812  ltleletr  8074  mulgt1  8855  fzind  9403  eqreznegel  9650  fzen  10079  elfzodifsumelfzo  10237  bernneq  10681  mulcn2  11361  prodmodclem2  11626  dvdsmod0  11841  divalglemeunn  11967  divalglemeuneg  11969  ndvdssub  11976  algcvgblem  12092  coprmdvds  12135  coprmdvds2  12136  divgcdcoprm0  12144  pceu  12338  dvdsprmpweqnn  12379  oddprmdvds  12397  infpnlem1  12402  imasaddfnlemg  12802  sgrpidmndm  12904  imasabl  13298  lmss  14231  lmtopcnp  14235  zabsle1  14886  bj-sbimedh  15009  bj-nnen2lp  15192