Theorem impd 252

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  291  imp4c  348  imp4d  349  imp5d  356  expimpd  360  expl  375  pm3.37  678  pm5.6r  912  3expib  1184  sbiedh  1760  equs5  1801  moexexdc  2083  rsp2  2482  moi  2867  reu6  2873  sbciegft  2939  prel12  3698  opthpr  3699  invdisj  3923  sowlin  4242  reusv1  4379  relop  4689  elres  4855  iss  4865  funssres  5165  fv3  5444  funfvima  5649  poxp  6129  tfri3  6264  nndi  6382  nnmass  6383  nnmordi  6412  nnmord  6413  eroveu  6520  fiintim  6817  suplubti  6887  addnq0mo  7255  mulnq0mo  7256  prcdnql  7292  prcunqu  7293  prnmaxl  7296  prnminu  7297  genprndl  7329  genprndu  7330  distrlem1prl  7390  distrlem1pru  7391  distrlem5prl  7394  distrlem5pru  7395  recexprlemss1l  7443  recexprlemss1u  7444  addsrmo  7551  mulsrmo  7552  mulgt0sr  7586  ltleletr  7846  mulgt1  8621  fzind  9166  eqreznegel  9406  fzen  9823  elfzodifsumelfzo  9978  bernneq  10412  mulcn2  11081  prodmodclem2  11346  divalglemeunn  11618  divalglemeuneg  11620  ndvdssub  11627  algcvgblem  11730  coprmdvds  11773  coprmdvds2  11774  divgcdcoprm0  11782  lmss  12415  lmtopcnp  12419  bj-sbimedh  12978  bj-nnen2lp  13152