Theorem expdimp 259

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
exp3a.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expdimp	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 258	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	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  ax-ia3 108

This theorem is referenced by:  rexlimdvv  2631  reu6  2963  fun11iun  5550  poxp  6325  smoel  6393  iinerm  6701  suplub2ti  7110  infglbti  7134  infnlbti  7135  prarloclemlo  7614  peano5uzti  9488  lbzbi  9744  ssfzo12bi  10361  cau3lem  11469  summodc  11738  mertenslem2  11891  prodmodclem2  11932  alzdvds  12209  nno  12261  nn0seqcvgd  12407  lcmdvds  12445  divgcdodd  12509  prmpwdvds  12722  cnptoprest  14755  lmss  14762  txlm  14795  incistruhgr  15730