Theorem imp4c 424

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp44  429  reuop  6251  omordi  8498  omwordri  8504  omass  8512  oewordri  8525  umgrclwwlkge2  30086  upgr4cycl4dv4e  30280  elspansn5  31670  atcvat3i  32492  mdsymlem5  32503  sumdmdlem  32514  regsfromregtco  36773  cvrat4  39942  2reuimp  47585  sprsymrelfolem2  47975  reupr  48004  grtriprop  48439  isubgr3stgrlem6  48469