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  2993  fun11iun  5601  poxp  6392  smoel  6461  iinerm  6771  suplub2ti  7194  infglbti  7218  infnlbti  7219  prarloclemlo  7707  peano5uzti  9581  lbzbi  9843  ssfzo12bi  10463  cau3lem  11668  summodc  11937  mertenslem2  12090  prodmodclem2  12131  alzdvds  12408  nno  12460  nn0seqcvgd  12606  lcmdvds  12644  divgcdodd  12708  prmpwdvds  12921  cnptoprest  14956  lmss  14963  txlm  14996  incistruhgr  15934