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  2621  reu6  2953  fun11iun  5528  poxp  6299  smoel  6367  iinerm  6675  suplub2ti  7076  infglbti  7100  infnlbti  7101  prarloclemlo  7580  peano5uzti  9453  lbzbi  9709  ssfzo12bi  10320  cau3lem  11298  summodc  11567  mertenslem2  11720  prodmodclem2  11761  alzdvds  12038  nno  12090  nn0seqcvgd  12236  lcmdvds  12274  divgcdodd  12338  prmpwdvds  12551  cnptoprest  14561  lmss  14568  txlm  14601