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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  289  imp4c  346  imp4d  347  imp5d  354  expimpd  358  expl  373  pm3.37  661  pm5.6r  893  3expib  1165  sbiedh  1741  equs5  1781  moexexdc  2057  rsp2  2454  moi  2834  reu6  2840  sbciegft  2905  prel12  3662  opthpr  3663  invdisj  3887  sowlin  4200  reusv1  4337  relop  4647  elres  4811  iss  4821  funssres  5121  fv3  5396  funfvima  5601  poxp  6081  tfri3  6216  nndi  6334  nnmass  6335  nnmordi  6364  nnmord  6365  eroveu  6472  fiintim  6768  suplubti  6837  addnq0mo  7197  mulnq0mo  7198  prcdnql  7234  prcunqu  7235  prnmaxl  7238  prnminu  7239  genprndl  7271  genprndu  7272  distrlem1prl  7332  distrlem1pru  7333  distrlem5prl  7336  distrlem5pru  7337  recexprlemss1l  7385  recexprlemss1u  7386  addsrmo  7480  mulsrmo  7481  mulgt0sr  7514  ltleletr  7763  mulgt1  8525  fzind  9064  eqreznegel  9302  fzen  9710  elfzodifsumelfzo  9865  bernneq  10299  mulcn2  10967  divalglemeunn  11460  divalglemeuneg  11462  ndvdssub  11469  algcvgblem  11570  coprmdvds  11613  coprmdvds2  11614  divgcdcoprm0  11622  lmss  12251  lmtopcnp  12255  bj-sbimedh  12662  bj-nnen2lp  12835