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  1381  ad5ant125OLD  1391  ad5ant2345  1397  peano5  7905  oelim  8542  lemul12a  12175  uzwo  13038  elfznelfzo  13908  injresinj  13926  swrdswrd  14854  2cshwcshw  14976  dvdsprmpweqle  17064  catidd  17854  grpinveu  19185  unichnlidl  21516  matunitlindflem1  22994  2ndcctbss  23774  rusgrnumwwlks  30566  erclwwlktr  30613  wwlksext2clwwlk  30648  erclwwlkntr  30662  grpoinveu  31121  spansncvi  32254  sumdmdii  33017  relowlpssretop  38287  unichnidl  38965  linepsubN  40809  pmapsub  40825  cdlemkid4  41991  hbtlem2  44125  2reu8i  48182  ply1mulgsumlem2  49498