Theorem imp4c 428

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 415	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	impd 415	1 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp44  433  reuop  6296  omordi  8552  omwordri  8558  omass  8566  oewordri  8579  umgrclwwlkge2  30320  upgr4cycl4dv4e  30514  elspansn5  31904  atcvat3i  32726  mdsymlem5  32737  sumdmdlem  32748  regsfromregtco  37027  cvrat4  40195  2reuimp  47829  sprsymrelfolem2  48219  reupr  48248  grtriprop  48683  isubgr3stgrlem6  48713