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 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rexlimdvv  2675  reu6  3015  ifeqeqxdc  3687  fun11iun  5660  poxp  6468  suppssrst  6501  suppssrgst  6502  smoel  6571  iinerm  6881  suplub2ti  7341  infglbti  7365  infnlbti  7366  prarloclemlo  7861  peano5uzti  9756  lbzbi  10018  ssfzo12bi  10645  cau3lem  11882  summodc  12152  mertenslem2  12305  prodmodclem2  12346  alzdvds  12623  nno  12675  nn0seqcvgd  12821  lcmdvds  12859  divgcdodd  12923  prmpwdvds  13136  cnptoprest  15342  lmss  15349  txlm  15382  incistruhgr  16343