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  2635  reu6  2972  fun11iun  5569  poxp  6348  smoel  6416  iinerm  6724  suplub2ti  7136  infglbti  7160  infnlbti  7161  prarloclemlo  7649  peano5uzti  9523  lbzbi  9779  ssfzo12bi  10398  cau3lem  11591  summodc  11860  mertenslem2  12013  prodmodclem2  12054  alzdvds  12331  nno  12383  nn0seqcvgd  12529  lcmdvds  12567  divgcdodd  12631  prmpwdvds  12844  cnptoprest  14878  lmss  14885  txlm  14918  incistruhgr  15855