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  3008  fun11iun  5637  poxp  6430  suppssrst  6463  suppssrgst  6464  smoel  6533  iinerm  6843  suplub2ti  7294  infglbti  7318  infnlbti  7319  prarloclemlo  7814  peano5uzti  9692  lbzbi  9954  ssfzo12bi  10577  cau3lem  11807  summodc  12077  mertenslem2  12230  prodmodclem2  12271  alzdvds  12548  nno  12600  nn0seqcvgd  12746  lcmdvds  12784  divgcdodd  12848  prmpwdvds  13061  cnptoprest  15153  lmss  15160  txlm  15193  incistruhgr  16134