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 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rexlimdvv  2675  reu6  3015  ifeqeqxdc  3687  fun11iun  5663  poxp  6472  suppssrst  6505  suppssrgst  6506  smoel  6575  iinerm  6885  suplub2ti  7348  infglbti  7372  infnlbti  7373  prarloclemlo  7868  peano5uzti  9766  lbzbi  10033  ssfzo12bi  10661  cau3lem  11904  summodc  12176  mertenslem2  12329  prodmodclem2  12370  alzdvds  12647  nno  12699  nn0seqcvgd  12845  lcmdvds  12883  divgcdodd  12948  prmpwdvds  13164  cnptoprest  15477  lmss  15484  txlm  15517  incistruhgr  16548