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  2556  reu6  2873  fun11iun  5388  poxp  6129  smoel  6197  iinerm  6501  suplub2ti  6888  infglbti  6912  infnlbti  6913  prarloclemlo  7302  peano5uzti  9159  lbzbi  9408  ssfzo12bi  10002  cau3lem  10886  summodc  11152  mertenslem2  11305  prodmodclem2  11346  alzdvds  11552  nno  11603  nn0seqcvgd  11722  lcmdvds  11760  divgcdodd  11821  cnptoprest  12408  lmss  12415  txlm  12448