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  690  pm5.6r  928  3expib  1208  sbiedh  1801  equs5  1843  moexexdc  2129  rsp2  2547  moi  2947  reu6  2953  sbciegft  3020  prel12  3802  opthpr  3803  invdisj  4028  sowlin  4356  reusv1  4494  relop  4817  elres  4983  iss  4993  funssres  5301  fv3  5584  funfvima  5797  poxp  6299  tfri3  6434  nndi  6553  nnmass  6554  nnmordi  6583  nnmord  6584  eroveu  6694  fiintim  7001  suplubti  7075  addnq0mo  7533  mulnq0mo  7534  prcdnql  7570  prcunqu  7571  prnmaxl  7574  prnminu  7575  genprndl  7607  genprndu  7608  distrlem1prl  7668  distrlem1pru  7669  distrlem5prl  7672  distrlem5pru  7673  recexprlemss1l  7721  recexprlemss1u  7722  addsrmo  7829  mulsrmo  7830  mulgt0sr  7864  ltleletr  8127  mulgt1  8909  fzind  9460  eqreznegel  9707  fzen  10137  elfzodifsumelfzo  10296  bernneq  10771  mulcn2  11496  prodmodclem2  11761  dvdsmod0  11977  divalglemeunn  12105  divalglemeuneg  12107  ndvdssub  12114  algcvgblem  12244  coprmdvds  12287  coprmdvds2  12288  divgcdcoprm0  12296  pceu  12491  dvdsprmpweqnn  12532  oddprmdvds  12550  infpnlem1  12555  imasaddfnlemg  13018  sgrpidmndm  13124  imasabl  13544  lmss  14590  lmtopcnp  14594  zabsle1  15348  2lgslem3  15450  bj-sbimedh  15525  bj-nnen2lp  15708