Theorem impd 251

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 80	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 122	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem is referenced by:  imp32  253  pm3.31  258  syland  287  imp4c  343  imp4d  344  imp5d  351  expimpd  355  expl  370  pm3.37  822  pm5.6r  870  3expib  1142  sbiedh  1711  equs5  1751  moexexdc  2026  rsp2  2414  moi  2776  reu6  2782  sbciegft  2845  prel12  3571  opthpr  3572  invdisj  3788  sowlin  4083  reusv1  4216  relop  4514  elres  4674  iss  4684  funssres  4972  fv3  5229  funfvima  5422  poxp  5884  tfri3  6016  nndi  6130  nnmass  6131  nnmordi  6155  nnmord  6156  eroveu  6263  suplubti  6472  addnq0mo  6699  mulnq0mo  6700  prcdnql  6736  prcunqu  6737  prnmaxl  6740  prnminu  6741  genprndl  6773  genprndu  6774  distrlem1prl  6834  distrlem1pru  6835  distrlem5prl  6838  distrlem5pru  6839  recexprlemss1l  6887  recexprlemss1u  6888  addsrmo  6982  mulsrmo  6983  mulgt0sr  7016  ltleletr  7260  mulgt1  8008  fzind  8543  eqreznegel  8780  fzen  9138  elfzodifsumelfzo  9287  bernneq  9690  mulcn2  10289  divalglemeunn  10465  divalglemeuneg  10467  ndvdssub  10474  algcvgblem  10575  coprmdvds  10618  coprmdvds2  10619  divgcdcoprm0  10627  bj-sbimedh  10733  bj-nnen2lp  10907