Theorem expdimp 255

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  rexlimdvv  2483  reu6  2781  fun11iun  5167  poxp  5873  smoel  5938  iinerm  6201  suplub2ti  6414  infglbti  6438  infnlbti  6439  prarloclemlo  6684  peano5uzti  8455  lbzbi  8701  ssfzo12bi  9234  cau3lem  10000  alzdvds  10254  nno  10306  nn0seqcvgd  10423  lcmdvds  10461  divgcdodd  10522