Theorem imp4c 427

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp4c	⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))

Proof of Theorem imp4c

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	impd 414	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	impd 414	1 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  imp44  432  reuop  6276  omordi  8530  omwordri  8536  omass  8544  oewordri  8557  umgrclwwlkge2  30139  upgr4cycl4dv4e  30333  elspansn5  31723  atcvat3i  32545  mdsymlem5  32556  sumdmdlem  32567  regsfromregtco  36862  cvrat4  40031  2reuimp  47673  sprsymrelfolem2  48063  reupr  48092  grtriprop  48527  isubgr3stgrlem6  48557