Theorem imp41 428

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3anassrs  1356  ad5ant125  1362  ad5ant2345  1366  peano5  7607  oelim  8161  lemul12a  11500  uzwo  12314  elfznelfzo  13145  injresinj  13161  swrdswrd  14069  2cshwcshw  14189  dvdsprmpweqle  16224  catidd  16953  grpinveu  18140  2ndcctbss  22065  rusgrnumwwlks  27755  erclwwlktr  27802  wwlksext2clwwlk  27838  erclwwlkntr  27852  grpoinveu  28298  spansncvi  29431  sumdmdii  30194  relowlpssretop  34647  matunitlindflem1  34890  unichnidl  35311  linepsubN  36890  pmapsub  36906  cdlemkid4  38072  hbtlem2  39731  2reu8i  43319  ply1mulgsumlem2  44448