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  1810  equs5  1852  moexexdc  2138  rsp2  2556  moi  2956  reu6  2962  sbciegft  3029  prel12  3812  opthpr  3813  invdisj  4038  sowlin  4368  reusv1  4506  relop  4829  elres  4996  iss  5006  funssres  5314  fv3  5601  funfvima  5818  poxp  6320  tfri3  6455  nndi  6574  nnmass  6575  nnmordi  6604  nnmord  6605  eroveu  6715  fiintim  7030  suplubti  7104  addnq0mo  7562  mulnq0mo  7563  prcdnql  7599  prcunqu  7600  prnmaxl  7603  prnminu  7604  genprndl  7636  genprndu  7637  distrlem1prl  7697  distrlem1pru  7698  distrlem5prl  7701  distrlem5pru  7702  recexprlemss1l  7750  recexprlemss1u  7751  addsrmo  7858  mulsrmo  7859  mulgt0sr  7893  ltleletr  8156  mulgt1  8938  fzind  9490  eqreznegel  9737  fzen  10167  elfzodifsumelfzo  10332  bernneq  10807  mulcn2  11656  prodmodclem2  11921  dvdsmod0  12137  divalglemeunn  12265  divalglemeuneg  12267  ndvdssub  12274  algcvgblem  12404  coprmdvds  12447  coprmdvds2  12448  divgcdcoprm0  12456  pceu  12651  dvdsprmpweqnn  12692  oddprmdvds  12710  infpnlem1  12715  imasaddfnlemg  13179  sgrpidmndm  13285  imasabl  13705  lmss  14751  lmtopcnp  14755  zabsle1  15509  2lgslem3  15611  bj-sbimedh  15744  bj-nnen2lp  15927