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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

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  693  pm5.6r  932  3expib  1230  sbiedh  1833  equs5  1875  moexexdc  2162  rsp2  2580  moi  2986  reu6  2992  sbciegft  3059  prel12  3849  opthpr  3850  invdisj  4076  sowlin  4411  reusv1  4549  relop  4872  elres  5041  iss  5051  funssres  5360  fv3  5652  funfvima  5875  poxp  6384  tfri3  6519  nndi  6640  nnmass  6641  nnmordi  6670  nnmord  6671  eroveu  6781  fiintim  7101  suplubti  7175  addnq0mo  7642  mulnq0mo  7643  prcdnql  7679  prcunqu  7680  prnmaxl  7683  prnminu  7684  genprndl  7716  genprndu  7717  distrlem1prl  7777  distrlem1pru  7778  distrlem5prl  7781  distrlem5pru  7782  recexprlemss1l  7830  recexprlemss1u  7831  addsrmo  7938  mulsrmo  7939  mulgt0sr  7973  ltleletr  8236  mulgt1  9018  fzind  9570  eqreznegel  9817  fzen  10247  elfzodifsumelfzo  10415  bernneq  10890  swrdswrdlem  11244  mulcn2  11831  prodmodclem2  12096  dvdsmod0  12312  divalglemeunn  12440  divalglemeuneg  12442  ndvdssub  12449  algcvgblem  12579  coprmdvds  12622  coprmdvds2  12623  divgcdcoprm0  12631  pceu  12826  dvdsprmpweqnn  12867  oddprmdvds  12885  infpnlem1  12890  imasaddfnlemg  13355  sgrpidmndm  13461  imasabl  13881  lmss  14928  lmtopcnp  14932  zabsle1  15686  2lgslem3  15788  uhgr2edg  16012  ushgredgedg  16032  ushgredgedgloop  16034  bj-sbimedh  16159  bj-nnen2lp  16341