Theorem impd 252

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 123	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  291  imp4c  348  imp4d  349  imp5d  356  expimpd  360  expl  375  pm3.37  678  pm5.6r  912  3expib  1184  sbiedh  1760  equs5  1801  moexexdc  2081  rsp2  2480  moi  2862  reu6  2868  sbciegft  2934  prel12  3693  opthpr  3694  invdisj  3918  sowlin  4237  reusv1  4374  relop  4684  elres  4850  iss  4860  funssres  5160  fv3  5437  funfvima  5642  poxp  6122  tfri3  6257  nndi  6375  nnmass  6376  nnmordi  6405  nnmord  6406  eroveu  6513  fiintim  6810  suplubti  6880  addnq0mo  7248  mulnq0mo  7249  prcdnql  7285  prcunqu  7286  prnmaxl  7289  prnminu  7290  genprndl  7322  genprndu  7323  distrlem1prl  7383  distrlem1pru  7384  distrlem5prl  7387  distrlem5pru  7388  recexprlemss1l  7436  recexprlemss1u  7437  addsrmo  7544  mulsrmo  7545  mulgt0sr  7579  ltleletr  7839  mulgt1  8614  fzind  9159  eqreznegel  9399  fzen  9816  elfzodifsumelfzo  9971  bernneq  10405  mulcn2  11074  divalglemeunn  11607  divalglemeuneg  11609  ndvdssub  11616  algcvgblem  11719  coprmdvds  11762  coprmdvds2  11763  divgcdcoprm0  11771  lmss  12404  lmtopcnp  12408  bj-sbimedh  12967  bj-nnen2lp  13141