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  2618  reu6  2949  fun11iun  5521  poxp  6285  smoel  6353  iinerm  6661  suplub2ti  7060  infglbti  7084  infnlbti  7085  prarloclemlo  7554  peano5uzti  9425  lbzbi  9681  ssfzo12bi  10292  cau3lem  11258  summodc  11526  mertenslem2  11679  prodmodclem2  11720  alzdvds  11996  nno  12047  nn0seqcvgd  12179  lcmdvds  12217  divgcdodd  12281  prmpwdvds  12493  cnptoprest  14407  lmss  14414  txlm  14447