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  695  pm5.6r  934  3expib  1232  sbiedh  1835  equs5  1877  moexexdc  2164  rsp2  2582  moi  2989  reu6  2995  sbciegft  3062  prel12  3854  opthpr  3855  invdisj  4081  sowlin  4417  reusv1  4555  relop  4880  elres  5049  iss  5059  funssres  5369  fv3  5662  funfvima  5885  poxp  6396  tfri3  6532  nndi  6653  nnmass  6654  nnmordi  6683  nnmord  6684  eroveu  6794  fiintim  7122  suplubti  7198  addnq0mo  7666  mulnq0mo  7667  prcdnql  7703  prcunqu  7704  prnmaxl  7707  prnminu  7708  genprndl  7740  genprndu  7741  distrlem1prl  7801  distrlem1pru  7802  distrlem5prl  7805  distrlem5pru  7806  recexprlemss1l  7854  recexprlemss1u  7855  addsrmo  7962  mulsrmo  7963  mulgt0sr  7997  ltleletr  8260  mulgt1  9042  fzind  9594  eqreznegel  9847  fzen  10277  elfzodifsumelfzo  10445  bernneq  10921  swrdswrdlem  11284  mulcn2  11872  prodmodclem2  12137  dvdsmod0  12353  divalglemeunn  12481  divalglemeuneg  12483  ndvdssub  12490  algcvgblem  12620  coprmdvds  12663  coprmdvds2  12664  divgcdcoprm0  12672  pceu  12867  dvdsprmpweqnn  12908  oddprmdvds  12926  infpnlem1  12931  imasaddfnlemg  13396  sgrpidmndm  13502  imasabl  13922  lmss  14969  lmtopcnp  14973  zabsle1  15727  2lgslem3  15829  uhgr2edg  16056  ushgredgedg  16076  ushgredgedgloop  16078  bj-sbimedh  16367  bj-nnen2lp  16549