Theorem impd 251

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 80	. . 3 |- ( ps -> ( ch -> ( ph -> th ) ) )
3	2	imp 122	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem is referenced by:  imp32  253  pm3.31  258  syland  287  imp4c  343  imp4d  344  imp5d  351  expimpd  355  expl  370  pm3.37  821  pm5.6r  869  3expib  1141  sbiedh  1710  equs5  1750  moexexdc  2025  rsp2  2413  moi  2775  reu6  2781  sbciegft  2844  prel12  3563  opthpr  3564  invdisj  3780  sowlin  4075  reusv1  4208  relop  4504  elres  4664  iss  4674  funssres  4962  fv3  5218  funfvima  5411  poxp  5873  tfri3  5976  nndi  6088  nnmass  6089  nnmordi  6112  nnmord  6113  eroveu  6220  suplubti  6413  addnq0mo  6637  mulnq0mo  6638  prcdnql  6674  prcunqu  6675  prnmaxl  6678  prnminu  6679  genprndl  6711  genprndu  6712  distrlem1prl  6772  distrlem1pru  6773  distrlem5prl  6776  distrlem5pru  6777  recexprlemss1l  6825  recexprlemss1u  6826  addsrmo  6920  mulsrmo  6921  mulgt0sr  6954  ltleletr  7193  mulgt1  7941  fzind  8462  eqreznegel  8699  fzen  9062  elfzodifsumelfzo  9210  bernneq  9593  mulcn2  10151  divalglemeunn  10321  divalglemeuneg  10323  ndvdssub  10330  algcvgblem  10431  coprmdvds  10474  coprmdvds2  10475  divgcdcoprm0  10483  bj-sbimedh  10582  bj-nnen2lp  10749