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  7891  oelim  8524  lemul12a  12100  uzwo  12963  elfznelfzo  13832  injresinj  13850  swrdswrd  14777  2cshwcshw  14899  dvdsprmpweqle  16981  catidd  17771  grpinveu  19101  unichnlidl  21428  matunitlindflem1  22904  2ndcctbss  23684  rusgrnumwwlks  30448  erclwwlktr  30495  wwlksext2clwwlk  30530  erclwwlkntr  30544  grpoinveu  31003  spansncvi  32136  sumdmdii  32899  relowlpssretop  38121  unichnidl  38784  linepsubN  40628  pmapsub  40644  cdlemkid4  41810  hbtlem2  43968  2reu8i  48004  ply1mulgsumlem2  49320