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 ) )

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

This theorem is used by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  700  pm5.6r  939  3expib  1237  sbiedh  1840  equs5  1882  moexexdc  2171  rsp2  2600  moi  3009  reu6  3015  sbciegft  3082  prel12  3896  opthpr  3897  invdisj  4123  sowlin  4467  reusv1  4606  relop  4932  elres  5101  iss  5112  funssres  5423  fv3  5721  funfvima  5953  poxp  6472  tfri3  6642  nndi  6763  nnmass  6764  nnmordi  6793  nnmord  6794  eroveu  6904  fiintim  7242  suplubti  7346  addnq0mo  7820  mulnq0mo  7821  prcdnql  7857  prcunqu  7858  prnmaxl  7861  prnminu  7862  genprndl  7894  genprndu  7895  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  recexprlemss1l  8008  recexprlemss1u  8009  addsrmo  8116  mulsrmo  8117  mulgt0sr  8151  ltleletr  8413  mulgt1  9201  fzind  9772  eqreznegel  10030  fzen  10464  elfzodifsumelfzo  10636  bernneq  11119  swrdswrdlem  11498  mulcn2  12103  prodmodclem2  12369  dvdsmod0  12585  divalglemeunn  12713  divalglemeuneg  12715  ndvdssub  12722  algcvgblem  12852  coprmdvds  12895  coprmdvds2  12896  divgcdcoprm0  12904  pceu  13103  dvdsprmpweqnn  13144  oddprmdvds  13162  infpnlem1  13167  imasaddfnlemg  13694  sgrpidmndm  13792  imasabl  14230  lmss  15472  lmtopcnp  15476  zabsle1  16323  2lgslem3  16425  uhgr2edg  16652  ushgredgedg  16672  ushgredgedgloop  16674  bj-sbimedh  17004  bj-nnen2lp  17185