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  700  pm5.6r  939  3expib  1237  sbiedh  1840  equs5  1882  moexexdc  2171  rsp2  2600  moi  3009  reu6  3015  sbciegft  3082  prel12  3891  opthpr  3892  invdisj  4118  sowlin  4460  reusv1  4599  relop  4925  elres  5094  iss  5104  funssres  5415  fv3  5713  funfvima  5940  poxp  6458  tfri3  6628  nndi  6749  nnmass  6750  nnmordi  6779  nnmord  6780  eroveu  6890  fiintim  7228  suplubti  7330  addnq0mo  7804  mulnq0mo  7805  prcdnql  7841  prcunqu  7842  prnmaxl  7845  prnminu  7846  genprndl  7878  genprndu  7879  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  recexprlemss1l  7992  recexprlemss1u  7993  addsrmo  8100  mulsrmo  8101  mulgt0sr  8135  ltleletr  8397  mulgt1  9183  fzind  9740  eqreznegel  9993  fzen  10426  elfzodifsumelfzo  10597  bernneq  11076  swrdswrdlem  11454  mulcn2  12056  prodmodclem2  12322  dvdsmod0  12538  divalglemeunn  12666  divalglemeuneg  12668  ndvdssub  12675  algcvgblem  12805  coprmdvds  12848  coprmdvds2  12849  divgcdcoprm0  12857  pceu  13052  dvdsprmpweqnn  13093  oddprmdvds  13111  infpnlem1  13116  imasaddfnlemg  13612  sgrpidmndm  13710  imasabl  14117  lmss  15270  lmtopcnp  15274  zabsle1  16032  2lgslem3  16134  uhgr2edg  16361  ushgredgedg  16381  ushgredgedgloop  16383  bj-sbimedh  16713  bj-nnen2lp  16894