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  826  pm5.6r  874  3expib  1146  sbiedh  1717  equs5  1757  moexexdc  2032  rsp2  2425  moi  2796  reu6  2802  sbciegft  2867  prel12  3610  opthpr  3611  invdisj  3831  sowlin  4138  reusv1  4271  relop  4574  elres  4735  iss  4745  funssres  5042  fv3  5312  funfvima  5508  poxp  5979  tfri3  6114  nndi  6229  nnmass  6230  nnmordi  6255  nnmord  6256  eroveu  6363  suplubti  6674  addnq0mo  6985  mulnq0mo  6986  prcdnql  7022  prcunqu  7023  prnmaxl  7026  prnminu  7027  genprndl  7059  genprndu  7060  distrlem1prl  7120  distrlem1pru  7121  distrlem5prl  7124  distrlem5pru  7125  recexprlemss1l  7173  recexprlemss1u  7174  addsrmo  7268  mulsrmo  7269  mulgt0sr  7302  ltleletr  7546  mulgt1  8296  fzind  8831  eqreznegel  9068  fzen  9426  elfzodifsumelfzo  9577  bernneq  10039  mulcn2  10665  divalglemeunn  11014  divalglemeuneg  11016  ndvdssub  11023  algcvgblem  11124  coprmdvds  11167  coprmdvds2  11168  divgcdcoprm0  11176  bj-sbimedh  11329  bj-nnen2lp  11506