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  2675  reu6  3015  ifeqeqxdc  3687  fun11iun  5658  poxp  6462  suppssrst  6495  suppssrgst  6496  smoel  6565  iinerm  6875  suplub2ti  7335  infglbti  7359  infnlbti  7360  prarloclemlo  7855  peano5uzti  9737  lbzbi  9999  ssfzo12bi  10626  cau3lem  11863  summodc  12133  mertenslem2  12286  prodmodclem2  12327  alzdvds  12604  nno  12656  nn0seqcvgd  12802  lcmdvds  12840  divgcdodd  12904  prmpwdvds  13117  cnptoprest  15323  lmss  15330  txlm  15363  incistruhgr  16314