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  691  pm5.6r  929  3expib  1209  sbiedh  1811  equs5  1853  moexexdc  2140  rsp2  2558  moi  2963  reu6  2969  sbciegft  3036  prel12  3825  opthpr  3826  invdisj  4052  sowlin  4385  reusv1  4523  relop  4846  elres  5014  iss  5024  funssres  5332  fv3  5622  funfvima  5839  poxp  6341  tfri3  6476  nndi  6595  nnmass  6596  nnmordi  6625  nnmord  6626  eroveu  6736  fiintim  7054  suplubti  7128  addnq0mo  7595  mulnq0mo  7596  prcdnql  7632  prcunqu  7633  prnmaxl  7636  prnminu  7637  genprndl  7669  genprndu  7670  distrlem1prl  7730  distrlem1pru  7731  distrlem5prl  7734  distrlem5pru  7735  recexprlemss1l  7783  recexprlemss1u  7784  addsrmo  7891  mulsrmo  7892  mulgt0sr  7926  ltleletr  8189  mulgt1  8971  fzind  9523  eqreznegel  9770  fzen  10200  elfzodifsumelfzo  10367  bernneq  10842  swrdswrdlem  11195  mulcn2  11738  prodmodclem2  12003  dvdsmod0  12219  divalglemeunn  12347  divalglemeuneg  12349  ndvdssub  12356  algcvgblem  12486  coprmdvds  12529  coprmdvds2  12530  divgcdcoprm0  12538  pceu  12733  dvdsprmpweqnn  12774  oddprmdvds  12792  infpnlem1  12797  imasaddfnlemg  13261  sgrpidmndm  13367  imasabl  13787  lmss  14833  lmtopcnp  14837  zabsle1  15591  2lgslem3  15693  bj-sbimedh  15907  bj-nnen2lp  16089