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  684  pm5.6r  922  3expib  1201  sbiedh  1780  equs5  1822  moexexdc  2103  rsp2  2520  moi  2913  reu6  2919  sbciegft  2985  prel12  3758  opthpr  3759  invdisj  3983  sowlin  4305  reusv1  4443  relop  4761  elres  4927  iss  4937  funssres  5240  fv3  5519  funfvima  5727  poxp  6211  tfri3  6346  nndi  6465  nnmass  6466  nnmordi  6495  nnmord  6496  eroveu  6604  fiintim  6906  suplubti  6977  addnq0mo  7409  mulnq0mo  7410  prcdnql  7446  prcunqu  7447  prnmaxl  7450  prnminu  7451  genprndl  7483  genprndu  7484  distrlem1prl  7544  distrlem1pru  7545  distrlem5prl  7548  distrlem5pru  7549  recexprlemss1l  7597  recexprlemss1u  7598  addsrmo  7705  mulsrmo  7706  mulgt0sr  7740  ltleletr  8001  mulgt1  8779  fzind  9327  eqreznegel  9573  fzen  9999  elfzodifsumelfzo  10157  bernneq  10596  mulcn2  11275  prodmodclem2  11540  dvdsmod0  11755  divalglemeunn  11880  divalglemeuneg  11882  ndvdssub  11889  algcvgblem  12003  coprmdvds  12046  coprmdvds2  12047  divgcdcoprm0  12055  pceu  12249  dvdsprmpweqnn  12289  oddprmdvds  12306  infpnlem1  12311  sgrpidmndm  12656  lmss  13040  lmtopcnp  13044  zabsle1  13694  bj-sbimedh  13806  bj-nnen2lp  13989