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  5652  funfvima  5875  poxp  6384  tfri3  6519  nndi  6640  nnmass  6641  nnmordi  6670  nnmord  6671  eroveu  6781  fiintim  7104  suplubti  7178  addnq0mo  7645  mulnq0mo  7646  prcdnql  7682  prcunqu  7683  prnmaxl  7686  prnminu  7687  genprndl  7719  genprndu  7720  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  recexprlemss1l  7833  recexprlemss1u  7834  addsrmo  7941  mulsrmo  7942  mulgt0sr  7976  ltleletr  8239  mulgt1  9021  fzind  9573  eqreznegel  9821  fzen  10251  elfzodifsumelfzo  10419  bernneq  10894  swrdswrdlem  11252  mulcn2  11839  prodmodclem2  12104  dvdsmod0  12320  divalglemeunn  12448  divalglemeuneg  12450  ndvdssub  12457  algcvgblem  12587  coprmdvds  12630  coprmdvds2  12631  divgcdcoprm0  12639  pceu  12834  dvdsprmpweqnn  12875  oddprmdvds  12893  infpnlem1  12898  imasaddfnlemg  13363  sgrpidmndm  13469  imasabl  13889  lmss  14936  lmtopcnp  14940  zabsle1  15694  2lgslem3  15796  uhgr2edg  16020  ushgredgedg  16040  ushgredgedgloop  16042  bj-sbimedh  16218  bj-nnen2lp  16400