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  6643  nndi  6764  nnmass  6765  nnmordi  6794  nnmord  6795  eroveu  6905  fiintim  7244  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  9771  eqreznegel  10029  fzen  10463  elfzodifsumelfzo  10635  bernneq  11118  swrdswrdlem  11497  mulcn2  12102  prodmodclem2  12368  dvdsmod0  12584  divalglemeunn  12712  divalglemeuneg  12714  ndvdssub  12721  algcvgblem  12851  coprmdvds  12894  coprmdvds2  12895  divgcdcoprm0  12903  pceu  13102  dvdsprmpweqnn  13143  oddprmdvds  13161  infpnlem1  13166  imasaddfnlemg  13693  sgrpidmndm  13791  imasabl  14229  lmss  15489  lmtopcnp  15493  zabsle1  16340  2lgslem3  16442  uhgr2edg  16669  ushgredgedg  16689  ushgredgedgloop  16691  bj-sbimedh  17021  bj-nnen2lp  17202