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  913  3expib  1185  sbiedh  1764  equs5  1806  moexexdc  2087  rsp2  2504  moi  2891  reu6  2897  sbciegft  2963  prel12  3730  opthpr  3731  invdisj  3955  sowlin  4275  reusv1  4412  relop  4729  elres  4895  iss  4905  funssres  5205  fv3  5484  funfvima  5689  poxp  6169  tfri3  6304  nndi  6422  nnmass  6423  nnmordi  6452  nnmord  6453  eroveu  6560  fiintim  6862  suplubti  6932  addnq0mo  7346  mulnq0mo  7347  prcdnql  7383  prcunqu  7384  prnmaxl  7387  prnminu  7388  genprndl  7420  genprndu  7421  distrlem1prl  7481  distrlem1pru  7482  distrlem5prl  7485  distrlem5pru  7486  recexprlemss1l  7534  recexprlemss1u  7535  addsrmo  7642  mulsrmo  7643  mulgt0sr  7677  ltleletr  7938  mulgt1  8713  fzind  9258  eqreznegel  9501  fzen  9923  elfzodifsumelfzo  10078  bernneq  10516  mulcn2  11186  prodmodclem2  11451  divalglemeunn  11785  divalglemeuneg  11787  ndvdssub  11794  algcvgblem  11898  coprmdvds  11941  coprmdvds2  11942  divgcdcoprm0  11950  lmss  12593  lmtopcnp  12597  bj-sbimedh  13291  bj-nnen2lp  13475