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  696  pm5.6r  935  3expib  1233  sbiedh  1835  equs5  1877  moexexdc  2164  rsp2  2583  moi  2990  reu6  2996  sbciegft  3063  prel12  3859  opthpr  3860  invdisj  4086  sowlin  4423  reusv1  4561  relop  4886  elres  5055  iss  5065  funssres  5376  fv3  5671  funfvima  5896  poxp  6406  tfri3  6576  nndi  6697  nnmass  6698  nnmordi  6727  nnmord  6728  eroveu  6838  fiintim  7166  suplubti  7259  addnq0mo  7727  mulnq0mo  7728  prcdnql  7764  prcunqu  7765  prnmaxl  7768  prnminu  7769  genprndl  7801  genprndu  7802  distrlem1prl  7862  distrlem1pru  7863  distrlem5prl  7866  distrlem5pru  7867  recexprlemss1l  7915  recexprlemss1u  7916  addsrmo  8023  mulsrmo  8024  mulgt0sr  8058  ltleletr  8320  mulgt1  9102  fzind  9656  eqreznegel  9909  fzen  10340  elfzodifsumelfzo  10509  bernneq  10985  swrdswrdlem  11351  mulcn2  11952  prodmodclem2  12218  dvdsmod0  12434  divalglemeunn  12562  divalglemeuneg  12564  ndvdssub  12571  algcvgblem  12701  coprmdvds  12744  coprmdvds2  12745  divgcdcoprm0  12753  pceu  12948  dvdsprmpweqnn  12989  oddprmdvds  13007  infpnlem1  13012  imasaddfnlemg  13477  sgrpidmndm  13583  imasabl  14003  lmss  15057  lmtopcnp  15061  zabsle1  15818  2lgslem3  15920  uhgr2edg  16147  ushgredgedg  16167  ushgredgedgloop  16169  bj-sbimedh  16489  bj-nnen2lp  16670