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  5598  poxp  6389  smoel  6457  iinerm  6767  suplub2ti  7184  infglbti  7208  infnlbti  7209  prarloclemlo  7697  peano5uzti  9571  lbzbi  9828  ssfzo12bi  10448  cau3lem  11646  summodc  11915  mertenslem2  12068  prodmodclem2  12109  alzdvds  12386  nno  12438  nn0seqcvgd  12584  lcmdvds  12622  divgcdodd  12686  prmpwdvds  12899  cnptoprest  14934  lmss  14941  txlm  14974  incistruhgr  15911