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  2657  reu6  2995  fun11iun  5604  poxp  6397  smoel  6466  iinerm  6776  suplub2ti  7200  infglbti  7224  infnlbti  7225  prarloclemlo  7714  peano5uzti  9588  lbzbi  9850  ssfzo12bi  10470  cau3lem  11675  summodc  11945  mertenslem2  12098  prodmodclem2  12139  alzdvds  12416  nno  12468  nn0seqcvgd  12614  lcmdvds  12652  divgcdodd  12716  prmpwdvds  12929  cnptoprest  14965  lmss  14972  txlm  15005  incistruhgr  15943