Theorem imp41 429

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  3anassrs  1362  ad5ant125  1368  ad5ant2345  1372  peano5  7671  peano5OLD  7672  oelim  8261  lemul12a  11690  uzwo  12507  elfznelfzo  13347  injresinj  13363  swrdswrd  14270  2cshwcshw  14390  dvdsprmpweqle  16439  catidd  17183  grpinveu  18402  2ndcctbss  22352  rusgrnumwwlks  28058  erclwwlktr  28105  wwlksext2clwwlk  28140  erclwwlkntr  28154  grpoinveu  28600  spansncvi  29733  sumdmdii  30496  relowlpssretop  35272  matunitlindflem1  35510  unichnidl  35926  linepsubN  37503  pmapsub  37519  cdlemkid4  38685  hbtlem2  40652  2reu8i  44277  ply1mulgsumlem2  45401