Theorem imp4c 423

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imp44  428  reuop  6257  omordi  8501  omwordri  8507  omass  8515  oewordri  8528  umgrclwwlkge2  30061  upgr4cycl4dv4e  30255  elspansn5  31645  atcvat3i  32467  mdsymlem5  32478  sumdmdlem  32489  regsfromregtco  36720  cvrat4  39889  2reuimp  47563  sprsymrelfolem2  47953  reupr  47982  grtriprop  48417  isubgr3stgrlem6  48447