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  6266  omordi  8530  omwordri  8536  omass  8544  oewordri  8556  umgrclwwlkge2  29920  upgr4cycl4dv4e  30114  elspansn5  31503  atcvat3i  32325  mdsymlem5  32336  sumdmdlem  32347  cvrat4  39437  2reuimp  47113  sprsymrelfolem2  47491  reupr  47520  grtriprop  47937  isubgr3stgrlem6  47967