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  4367  reusv1  4505  relop  4828  elres  4995  iss  5005  funssres  5313  fv3  5599  funfvima  5816  poxp  6318  tfri3  6453  nndi  6572  nnmass  6573  nnmordi  6602  nnmord  6603  eroveu  6713  fiintim  7028  suplubti  7102  addnq0mo  7560  mulnq0mo  7561  prcdnql  7597  prcunqu  7598  prnmaxl  7601  prnminu  7602  genprndl  7634  genprndu  7635  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  recexprlemss1l  7748  recexprlemss1u  7749  addsrmo  7856  mulsrmo  7857  mulgt0sr  7891  ltleletr  8154  mulgt1  8936  fzind  9488  eqreznegel  9735  fzen  10165  elfzodifsumelfzo  10330  bernneq  10805  mulcn2  11623  prodmodclem2  11888  dvdsmod0  12104  divalglemeunn  12232  divalglemeuneg  12234  ndvdssub  12241  algcvgblem  12371  coprmdvds  12414  coprmdvds2  12415  divgcdcoprm0  12423  pceu  12618  dvdsprmpweqnn  12659  oddprmdvds  12677  infpnlem1  12682  imasaddfnlemg  13146  sgrpidmndm  13252  imasabl  13672  lmss  14718  lmtopcnp  14722  zabsle1  15476  2lgslem3  15578  bj-sbimedh  15707  bj-nnen2lp  15890