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  6295  omordi  8557  omwordri  8563  omass  8571  oewordri  8584  umgrclwwlkge2  30469  upgr4cycl4dv4e  30673  elspansn5  32063  atcvat3i  32885  mdsymlem5  32896  sumdmdlem  32907  regsfromregtco  37165  cvrat4  40324  2reuimp  48011  sprsymrelfolem2  48401  reupr  48430  grtriprop  48865  isubgr3stgrlem6  48895