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  6251  omordi  8494  omwordri  8500  omass  8508  oewordri  8521  umgrclwwlkge2  30076  upgr4cycl4dv4e  30270  elspansn5  31660  atcvat3i  32482  mdsymlem5  32493  sumdmdlem  32504  regsfromregtco  36736  cvrat4  39903  2reuimp  47575  sprsymrelfolem2  47965  reupr  47994  grtriprop  48429  isubgr3stgrlem6  48459