Theorem imp4c 429

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp44  434  reuop  6296  omordi  8577  omwordri  8583  omass  8591  oewordri  8604  umgrclwwlkge2  30587  upgr4cycl4dv4e  30791  elspansn5  32181  atcvat3i  33003  mdsymlem5  33014  sumdmdlem  33025  regsfromregtco  37418  cvrat4  40593  2reuimp  48278  sprsymrelfolem2  48668  reupr  48697  grtriprop  49132  isubgr3stgrlem6  49162