Theorem impd 254

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
imp3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		imp3.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3l 81	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 124	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  700  pm5.6r  939  3expib  1237  sbiedh  1840  equs5  1882  moexexdc  2171  rsp2  2600  moi  3009  reu6  3015  sbciegft  3082  prel12  3896  opthpr  3897  invdisj  4123  sowlin  4467  reusv1  4606  relop  4932  elres  5101  iss  5112  funssres  5423  fv3  5721  funfvima  5953  poxp  6472  tfri3  6642  nndi  6763  nnmass  6764  nnmordi  6793  nnmord  6794  eroveu  6904  fiintim  7243  suplubti  7347  addnq0mo  7821  mulnq0mo  7822  prcdnql  7858  prcunqu  7859  prnmaxl  7862  prnminu  7863  genprndl  7895  genprndu  7896  distrlem1prl  7956  distrlem1pru  7957  distrlem5prl  7960  distrlem5pru  7961  recexprlemss1l  8009  recexprlemss1u  8010  addsrmo  8117  mulsrmo  8118  mulgt0sr  8152  ltleletr  8414  mulgt1  9202  fzind  9773  eqreznegel  10031  fzen  10465  elfzodifsumelfzo  10637  bernneq  11120  swrdswrdlem  11499  mulcn2  12104  prodmodclem2  12370  dvdsmod0  12586  divalglemeunn  12714  divalglemeuneg  12716  ndvdssub  12723  algcvgblem  12853  coprmdvds  12896  coprmdvds2  12897  divgcdcoprm0  12905  pceu  13104  dvdsprmpweqnn  13145  oddprmdvds  13163  infpnlem1  13168  imasaddfnlemg  13695  sgrpidmndm  13793  imasabl  14231  lmss  15484  lmtopcnp  15488  zabsle1  16335  2lgslem3  16437  uhgr2edg  16664  ushgredgedg  16684  ushgredgedgloop  16686  bj-sbimedh  17016  bj-nnen2lp  17197