Theorem imp41 431

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp41	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem imp41

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	imp31 423	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:  3anassrs  1382  ad5ant125OLD  1392  ad5ant2345  1398  peano5  7939  oelim  8580  lemul12a  12215  uzwo  13078  elfznelfzo  13948  injresinj  13966  swrdswrd  14896  2cshwcshw  15018  dvdsprmpweqle  17108  catidd  17904  grpinveu  19235  unichnlidl  21567  matunitlindflem1  23049  2ndcctbss  23829  rusgrnumwwlks  30623  erclwwlktr  30670  wwlksext2clwwlk  30705  erclwwlkntr  30719  grpoinveu  31178  spansncvi  32311  sumdmdii  33074  relowlpssretop  38555  unichnidl  39231  linepsubN  41075  pmapsub  41091  cdlemkid4  42257  hbtlem2  44391  2reu8i  48457  ply1mulgsumlem2  49830