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  690  pm5.6r  928  3expib  1208  sbiedh  1798  equs5  1840  moexexdc  2126  rsp2  2544  moi  2943  reu6  2949  sbciegft  3016  prel12  3797  opthpr  3798  invdisj  4023  sowlin  4351  reusv1  4489  relop  4812  elres  4978  iss  4988  funssres  5296  fv3  5577  funfvima  5790  poxp  6285  tfri3  6420  nndi  6539  nnmass  6540  nnmordi  6569  nnmord  6570  eroveu  6680  fiintim  6985  suplubti  7059  addnq0mo  7507  mulnq0mo  7508  prcdnql  7544  prcunqu  7545  prnmaxl  7548  prnminu  7549  genprndl  7581  genprndu  7582  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  recexprlemss1l  7695  recexprlemss1u  7696  addsrmo  7803  mulsrmo  7804  mulgt0sr  7838  ltleletr  8101  mulgt1  8882  fzind  9432  eqreznegel  9679  fzen  10109  elfzodifsumelfzo  10268  bernneq  10731  mulcn2  11455  prodmodclem2  11720  dvdsmod0  11936  divalglemeunn  12062  divalglemeuneg  12064  ndvdssub  12071  algcvgblem  12187  coprmdvds  12230  coprmdvds2  12231  divgcdcoprm0  12239  pceu  12433  dvdsprmpweqnn  12474  oddprmdvds  12492  infpnlem1  12497  imasaddfnlemg  12897  sgrpidmndm  13001  imasabl  13406  lmss  14414  lmtopcnp  14418  zabsle1  15115  bj-sbimedh  15263  bj-nnen2lp  15446