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  4465  reusv1  4604  relop  4930  elres  5099  iss  5109  funssres  5420  fv3  5718  funfvima  5950  poxp  6468  tfri3  6638  nndi  6759  nnmass  6760  nnmordi  6789  nnmord  6790  eroveu  6900  fiintim  7238  suplubti  7340  addnq0mo  7814  mulnq0mo  7815  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  genprndl  7888  genprndu  7889  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  recexprlemss1l  8002  recexprlemss1u  8003  addsrmo  8110  mulsrmo  8111  mulgt0sr  8145  ltleletr  8407  mulgt1  9195  fzind  9765  eqreznegel  10023  fzen  10457  elfzodifsumelfzo  10629  bernneq  11111  swrdswrdlem  11490  mulcn2  12094  prodmodclem2  12360  dvdsmod0  12576  divalglemeunn  12704  divalglemeuneg  12706  ndvdssub  12713  algcvgblem  12843  coprmdvds  12886  coprmdvds2  12887  divgcdcoprm0  12895  pceu  13094  dvdsprmpweqnn  13135  oddprmdvds  13153  infpnlem1  13158  imasaddfnlemg  13684  sgrpidmndm  13782  imasabl  14189  lmss  15396  lmtopcnp  15400  zabsle1  16216  2lgslem3  16318  uhgr2edg  16545  ushgredgedg  16565  ushgredgedgloop  16567  bj-sbimedh  16897  bj-nnen2lp  17078