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  9193  fzind  9761  eqreznegel  10014  fzen  10447  elfzodifsumelfzo  10619  bernneq  11098  swrdswrdlem  11476  mulcn2  12078  prodmodclem2  12344  dvdsmod0  12560  divalglemeunn  12688  divalglemeuneg  12690  ndvdssub  12697  algcvgblem  12827  coprmdvds  12870  coprmdvds2  12871  divgcdcoprm0  12879  pceu  13074  dvdsprmpweqnn  13115  oddprmdvds  13133  infpnlem1  13138  imasaddfnlemg  13635  sgrpidmndm  13733  imasabl  14140  lmss  15347  lmtopcnp  15351  zabsle1  16118  2lgslem3  16220  uhgr2edg  16447  ushgredgedg  16467  ushgredgedgloop  16469  bj-sbimedh  16799  bj-nnen2lp  16980