Theorem imp41 426

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 407	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	imp31 418	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  3anassrs  1359  ad5ant125  1365  ad5ant2345  1369  peano5  7787  peano5OLD  7788  oelim  8414  lemul12a  11913  uzwo  12731  elfznelfzo  13572  injresinj  13588  swrdswrd  14497  2cshwcshw  14617  dvdsprmpweqle  16664  catidd  17466  grpinveu  18690  2ndcctbss  22689  rusgrnumwwlks  28475  erclwwlktr  28522  wwlksext2clwwlk  28557  erclwwlkntr  28571  grpoinveu  29017  spansncvi  30150  sumdmdii  30913  relowlpssretop  35607  matunitlindflem1  35845  unichnidl  36261  linepsubN  37987  pmapsub  38003  cdlemkid4  39169  hbtlem2  41166  2reu8i  44870  ply1mulgsumlem2  45993