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  2655  reu6  2992  fun11iun  5595  poxp  6384  smoel  6452  iinerm  6762  suplub2ti  7176  infglbti  7200  infnlbti  7201  prarloclemlo  7689  peano5uzti  9563  lbzbi  9819  ssfzo12bi  10439  cau3lem  11633  summodc  11902  mertenslem2  12055  prodmodclem2  12096  alzdvds  12373  nno  12425  nn0seqcvgd  12571  lcmdvds  12609  divgcdodd  12673  prmpwdvds  12886  cnptoprest  14921  lmss  14928  txlm  14961  incistruhgr  15898