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 ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  690  pm5.6r  928  3expib  1208  sbiedh  1801  equs5  1843  moexexdc  2129  rsp2  2547  moi  2947  reu6  2953  sbciegft  3020  prel12  3802  opthpr  3803  invdisj  4028  sowlin  4356  reusv1  4494  relop  4817  elres  4983  iss  4993  funssres  5301  fv3  5584  funfvima  5797  poxp  6299  tfri3  6434  nndi  6553  nnmass  6554  nnmordi  6583  nnmord  6584  eroveu  6694  fiintim  7001  suplubti  7075  addnq0mo  7531  mulnq0mo  7532  prcdnql  7568  prcunqu  7569  prnmaxl  7572  prnminu  7573  genprndl  7605  genprndu  7606  distrlem1prl  7666  distrlem1pru  7667  distrlem5prl  7670  distrlem5pru  7671  recexprlemss1l  7719  recexprlemss1u  7720  addsrmo  7827  mulsrmo  7828  mulgt0sr  7862  ltleletr  8125  mulgt1  8907  fzind  9458  eqreznegel  9705  fzen  10135  elfzodifsumelfzo  10294  bernneq  10769  mulcn2  11494  prodmodclem2  11759  dvdsmod0  11975  divalglemeunn  12103  divalglemeuneg  12105  ndvdssub  12112  algcvgblem  12242  coprmdvds  12285  coprmdvds2  12286  divgcdcoprm0  12294  pceu  12489  dvdsprmpweqnn  12530  oddprmdvds  12548  infpnlem1  12553  imasaddfnlemg  13016  sgrpidmndm  13122  imasabl  13542  lmss  14566  lmtopcnp  14570  zabsle1  15324  2lgslem3  15426  bj-sbimedh  15501  bj-nnen2lp  15684