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  2601  reu6  2928  fun11iun  5484  poxp  6235  smoel  6303  iinerm  6609  suplub2ti  7002  infglbti  7026  infnlbti  7027  prarloclemlo  7495  peano5uzti  9363  lbzbi  9618  ssfzo12bi  10227  cau3lem  11125  summodc  11393  mertenslem2  11546  prodmodclem2  11587  alzdvds  11862  nno  11913  nn0seqcvgd  12043  lcmdvds  12081  divgcdodd  12145  prmpwdvds  12355  cnptoprest  13824  lmss  13831  txlm  13864