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  2669  reu6  3009  ifeqeqxdc  3673  fun11iun  5640  poxp  6441  suppssrst  6474  suppssrgst  6475  smoel  6544  iinerm  6854  suplub2ti  7305  infglbti  7329  infnlbti  7330  prarloclemlo  7825  peano5uzti  9707  lbzbi  9969  ssfzo12bi  10595  cau3lem  11827  summodc  12097  mertenslem2  12250  prodmodclem2  12291  alzdvds  12568  nno  12620  nn0seqcvgd  12766  lcmdvds  12804  divgcdodd  12868  prmpwdvds  13081  cnptoprest  15233  lmss  15240  txlm  15273  incistruhgr  16214