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  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2987  reu6  2993  sbciegft  3060  prel12  3852  opthpr  3853  invdisj  4079  sowlin  4415  reusv1  4553  relop  4878  elres  5047  iss  5057  funssres  5366  fv3  5658  funfvima  5881  poxp  6392  tfri3  6528  nndi  6649  nnmass  6650  nnmordi  6679  nnmord  6680  eroveu  6790  fiintim  7116  suplubti  7190  addnq0mo  7657  mulnq0mo  7658  prcdnql  7694  prcunqu  7695  prnmaxl  7698  prnminu  7699  genprndl  7731  genprndu  7732  distrlem1prl  7792  distrlem1pru  7793  distrlem5prl  7796  distrlem5pru  7797  recexprlemss1l  7845  recexprlemss1u  7846  addsrmo  7953  mulsrmo  7954  mulgt0sr  7988  ltleletr  8251  mulgt1  9033  fzind  9585  eqreznegel  9838  fzen  10268  elfzodifsumelfzo  10436  bernneq  10912  swrdswrdlem  11275  mulcn2  11863  prodmodclem2  12128  dvdsmod0  12344  divalglemeunn  12472  divalglemeuneg  12474  ndvdssub  12481  algcvgblem  12611  coprmdvds  12654  coprmdvds2  12655  divgcdcoprm0  12663  pceu  12858  dvdsprmpweqnn  12899  oddprmdvds  12917  infpnlem1  12922  imasaddfnlemg  13387  sgrpidmndm  13493  imasabl  13913  lmss  14960  lmtopcnp  14964  zabsle1  15718  2lgslem3  15820  uhgr2edg  16045  ushgredgedg  16065  ushgredgedgloop  16067  bj-sbimedh  16303  bj-nnen2lp  16485