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  689  pm5.6r  927  3expib  1206  sbiedh  1787  equs5  1829  moexexdc  2110  rsp2  2527  moi  2921  reu6  2927  sbciegft  2994  prel12  3772  opthpr  3773  invdisj  3998  sowlin  4321  reusv1  4459  relop  4778  elres  4944  iss  4954  funssres  5259  fv3  5539  funfvima  5749  poxp  6233  tfri3  6368  nndi  6487  nnmass  6488  nnmordi  6517  nnmord  6518  eroveu  6626  fiintim  6928  suplubti  6999  addnq0mo  7446  mulnq0mo  7447  prcdnql  7483  prcunqu  7484  prnmaxl  7487  prnminu  7488  genprndl  7520  genprndu  7521  distrlem1prl  7581  distrlem1pru  7582  distrlem5prl  7585  distrlem5pru  7586  recexprlemss1l  7634  recexprlemss1u  7635  addsrmo  7742  mulsrmo  7743  mulgt0sr  7777  ltleletr  8039  mulgt1  8820  fzind  9368  eqreznegel  9614  fzen  10043  elfzodifsumelfzo  10201  bernneq  10641  mulcn2  11320  prodmodclem2  11585  dvdsmod0  11800  divalglemeunn  11926  divalglemeuneg  11928  ndvdssub  11935  algcvgblem  12049  coprmdvds  12092  coprmdvds2  12093  divgcdcoprm0  12101  pceu  12295  dvdsprmpweqnn  12335  oddprmdvds  12352  infpnlem1  12357  imasaddfnlemg  12735  sgrpidmndm  12821  lmss  13749  lmtopcnp  13753  zabsle1  14403  bj-sbimedh  14526  bj-nnen2lp  14709