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  2656  reu6  2994  fun11iun  5607  poxp  6402  smoel  6471  iinerm  6781  suplub2ti  7205  infglbti  7229  infnlbti  7230  prarloclemlo  7719  peano5uzti  9593  lbzbi  9855  ssfzo12bi  10476  cau3lem  11697  summodc  11967  mertenslem2  12120  prodmodclem2  12161  alzdvds  12438  nno  12490  nn0seqcvgd  12636  lcmdvds  12674  divgcdodd  12738  prmpwdvds  12951  cnptoprest  14992  lmss  14999  txlm  15032  incistruhgr  15970