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  696  pm5.6r  935  3expib  1233  sbiedh  1836  equs5  1878  moexexdc  2165  rsp2  2592  moi  3000  reu6  3006  sbciegft  3073  prel12  3875  opthpr  3876  invdisj  4102  sowlin  4441  reusv1  4579  relop  4905  elres  5074  iss  5084  funssres  5395  fv3  5693  funfvima  5918  poxp  6428  tfri3  6598  nndi  6719  nnmass  6720  nnmordi  6749  nnmord  6750  eroveu  6860  fiintim  7191  suplubti  7291  addnq0mo  7762  mulnq0mo  7763  prcdnql  7799  prcunqu  7800  prnmaxl  7803  prnminu  7804  genprndl  7836  genprndu  7837  distrlem1prl  7897  distrlem1pru  7898  distrlem5prl  7901  distrlem5pru  7902  recexprlemss1l  7950  recexprlemss1u  7951  addsrmo  8058  mulsrmo  8059  mulgt0sr  8093  ltleletr  8355  mulgt1  9137  fzind  9693  eqreznegel  9946  fzen  10377  elfzodifsumelfzo  10546  bernneq  11022  swrdswrdlem  11396  mulcn2  11997  prodmodclem2  12263  dvdsmod0  12479  divalglemeunn  12607  divalglemeuneg  12609  ndvdssub  12616  algcvgblem  12746  coprmdvds  12789  coprmdvds2  12790  divgcdcoprm0  12798  pceu  12993  dvdsprmpweqnn  13034  oddprmdvds  13052  infpnlem1  13057  imasaddfnlemg  13527  sgrpidmndm  13633  imasabl  14053  lmss  15111  lmtopcnp  15115  zabsle1  15872  2lgslem3  15974  uhgr2edg  16201  ushgredgedg  16221  ushgredgedgloop  16223  bj-sbimedh  16543  bj-nnen2lp  16724