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  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2986  reu6  2992  sbciegft  3059  prel12  3849  opthpr  3850  invdisj  4076  sowlin  4411  reusv1  4549  relop  4872  elres  5041  iss  5051  funssres  5360  fv3  5650  funfvima  5871  poxp  6378  tfri3  6513  nndi  6632  nnmass  6633  nnmordi  6662  nnmord  6663  eroveu  6773  fiintim  7093  suplubti  7167  addnq0mo  7634  mulnq0mo  7635  prcdnql  7671  prcunqu  7672  prnmaxl  7675  prnminu  7676  genprndl  7708  genprndu  7709  distrlem1prl  7769  distrlem1pru  7770  distrlem5prl  7773  distrlem5pru  7774  recexprlemss1l  7822  recexprlemss1u  7823  addsrmo  7930  mulsrmo  7931  mulgt0sr  7965  ltleletr  8228  mulgt1  9010  fzind  9562  eqreznegel  9809  fzen  10239  elfzodifsumelfzo  10407  bernneq  10882  swrdswrdlem  11236  mulcn2  11823  prodmodclem2  12088  dvdsmod0  12304  divalglemeunn  12432  divalglemeuneg  12434  ndvdssub  12441  algcvgblem  12571  coprmdvds  12614  coprmdvds2  12615  divgcdcoprm0  12623  pceu  12818  dvdsprmpweqnn  12859  oddprmdvds  12877  infpnlem1  12882  imasaddfnlemg  13347  sgrpidmndm  13453  imasabl  13873  lmss  14920  lmtopcnp  14924  zabsle1  15678  2lgslem3  15780  uhgr2edg  16004  ushgredgedg  16024  ushgredgedgloop  16026  bj-sbimedh  16135  bj-nnen2lp  16317