Theorem expdimp 256

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  rexlimdvv  2496  reu6  2805  fun11iun  5287  poxp  6011  smoel  6079  iinerm  6378  suplub2ti  6750  infglbti  6774  infnlbti  6775  prarloclemlo  7114  peano5uzti  8915  lbzbi  9162  ssfzo12bi  9697  cau3lem  10608  isummo  10834  mertenslem2  10991  alzdvds  11194  nno  11245  nn0seqcvgd  11362  lcmdvds  11400  divgcdodd  11461