Theorem expdimp 257

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 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rexlimdvv  2554  reu6  2868  fun11iun  5381  poxp  6122  smoel  6190  iinerm  6494  suplub2ti  6881  infglbti  6905  infnlbti  6906  prarloclemlo  7295  peano5uzti  9152  lbzbi  9401  ssfzo12bi  9995  cau3lem  10879  summodc  11145  mertenslem2  11298  alzdvds  11541  nno  11592  nn0seqcvgd  11711  lcmdvds  11749  divgcdodd  11810  cnptoprest  12397  lmss  12404  txlm  12437