Theorem expdimp 257

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 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rexlimdvv  2559  reu6  2877  fun11iun  5396  poxp  6137  smoel  6205  iinerm  6509  suplub2ti  6896  infglbti  6920  infnlbti  6921  prarloclemlo  7326  peano5uzti  9183  lbzbi  9435  ssfzo12bi  10033  cau3lem  10918  summodc  11184  mertenslem2  11337  prodmodclem2  11378  alzdvds  11588  nno  11639  nn0seqcvgd  11758  lcmdvds  11796  divgcdodd  11857  cnptoprest  12447  lmss  12454  txlm  12487