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  2139  rsp2  2557  moi  2960  reu6  2966  sbciegft  3033  prel12  3818  opthpr  3819  invdisj  4044  sowlin  4375  reusv1  4513  relop  4836  elres  5004  iss  5014  funssres  5322  fv3  5612  funfvima  5829  poxp  6331  tfri3  6466  nndi  6585  nnmass  6586  nnmordi  6615  nnmord  6616  eroveu  6726  fiintim  7043  suplubti  7117  addnq0mo  7580  mulnq0mo  7581  prcdnql  7617  prcunqu  7618  prnmaxl  7621  prnminu  7622  genprndl  7654  genprndu  7655  distrlem1prl  7715  distrlem1pru  7716  distrlem5prl  7719  distrlem5pru  7720  recexprlemss1l  7768  recexprlemss1u  7769  addsrmo  7876  mulsrmo  7877  mulgt0sr  7911  ltleletr  8174  mulgt1  8956  fzind  9508  eqreznegel  9755  fzen  10185  elfzodifsumelfzo  10352  bernneq  10827  swrdswrdlem  11180  mulcn2  11698  prodmodclem2  11963  dvdsmod0  12179  divalglemeunn  12307  divalglemeuneg  12309  ndvdssub  12316  algcvgblem  12446  coprmdvds  12489  coprmdvds2  12490  divgcdcoprm0  12498  pceu  12693  dvdsprmpweqnn  12734  oddprmdvds  12752  infpnlem1  12757  imasaddfnlemg  13221  sgrpidmndm  13327  imasabl  13747  lmss  14793  lmtopcnp  14797  zabsle1  15551  2lgslem3  15653  bj-sbimedh  15846  bj-nnen2lp  16028