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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  imp32  254  pm3.31  259  syland  288  imp4c  344  imp4d  345  imp5d  352  expimpd  356  expl  371  pm3.37  829  pm5.6r  877  3expib  1149  sbiedh  1724  equs5  1764  moexexdc  2039  rsp2  2436  moi  2812  reu6  2818  sbciegft  2883  prel12  3637  opthpr  3638  invdisj  3861  sowlin  4171  reusv1  4308  relop  4617  elres  4781  iss  4791  funssres  5090  fv3  5363  funfvima  5565  poxp  6035  tfri3  6170  nndi  6287  nnmass  6288  nnmordi  6315  nnmord  6316  eroveu  6423  fiintim  6719  suplubti  6775  addnq0mo  7103  mulnq0mo  7104  prcdnql  7140  prcunqu  7141  prnmaxl  7144  prnminu  7145  genprndl  7177  genprndu  7178  distrlem1prl  7238  distrlem1pru  7239  distrlem5prl  7242  distrlem5pru  7243  recexprlemss1l  7291  recexprlemss1u  7292  addsrmo  7386  mulsrmo  7387  mulgt0sr  7420  ltleletr  7664  mulgt1  8421  fzind  8960  eqreznegel  9198  fzen  9606  elfzodifsumelfzo  9761  bernneq  10205  mulcn2  10871  divalglemeunn  11364  divalglemeuneg  11366  ndvdssub  11373  algcvgblem  11474  coprmdvds  11517  coprmdvds2  11518  divgcdcoprm0  11526  lmss  12113  lmtopcnp  12117  bj-sbimedh  12396  bj-nnen2lp  12573