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  2667  reu6  3005  fun11iun  5634  poxp  6427  suppssrst  6460  suppssrgst  6461  smoel  6530  iinerm  6840  suplub2ti  7291  infglbti  7315  infnlbti  7316  prarloclemlo  7805  peano5uzti  9682  lbzbi  9944  ssfzo12bi  10566  cau3lem  11792  summodc  12062  mertenslem2  12215  prodmodclem2  12256  alzdvds  12533  nno  12585  nn0seqcvgd  12731  lcmdvds  12769  divgcdodd  12833  prmpwdvds  13046  cnptoprest  15091  lmss  15098  txlm  15131  incistruhgr  16072