Theorem impd 252

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 123	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  291  imp4c  349  imp4d  350  imp5d  357  expimpd  361  expl  376  pm3.37  679  pm5.6r  917  3expib  1196  sbiedh  1775  equs5  1817  moexexdc  2098  rsp2  2515  moi  2908  reu6  2914  sbciegft  2980  prel12  3750  opthpr  3751  invdisj  3975  sowlin  4297  reusv1  4435  relop  4753  elres  4919  iss  4929  funssres  5229  fv3  5508  funfvima  5715  poxp  6196  tfri3  6331  nndi  6450  nnmass  6451  nnmordi  6480  nnmord  6481  eroveu  6588  fiintim  6890  suplubti  6961  addnq0mo  7384  mulnq0mo  7385  prcdnql  7421  prcunqu  7422  prnmaxl  7425  prnminu  7426  genprndl  7458  genprndu  7459  distrlem1prl  7519  distrlem1pru  7520  distrlem5prl  7523  distrlem5pru  7524  recexprlemss1l  7572  recexprlemss1u  7573  addsrmo  7680  mulsrmo  7681  mulgt0sr  7715  ltleletr  7976  mulgt1  8754  fzind  9302  eqreznegel  9548  fzen  9974  elfzodifsumelfzo  10132  bernneq  10571  mulcn2  11249  prodmodclem2  11514  dvdsmod0  11729  divalglemeunn  11854  divalglemeuneg  11856  ndvdssub  11863  algcvgblem  11977  coprmdvds  12020  coprmdvds2  12021  divgcdcoprm0  12029  pceu  12223  dvdsprmpweqnn  12263  oddprmdvds  12280  infpnlem1  12285  lmss  12846  lmtopcnp  12850  zabsle1  13500  bj-sbimedh  13612  bj-nnen2lp  13796