Theorem imp41 425

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3anassrs  1362  ad5ant125  1369  ad5ant2345  1373  peano5  7838  oelim  8463  lemul12a  12007  uzwo  12855  elfznelfzo  13722  injresinj  13740  swrdswrd  14661  2cshwcshw  14781  dvdsprmpweqle  16851  catidd  17640  grpinveu  18944  2ndcctbss  23433  rusgrnumwwlks  30063  erclwwlktr  30110  wwlksext2clwwlk  30145  erclwwlkntr  30159  grpoinveu  30608  spansncvi  31741  sumdmdii  32504  relowlpssretop  37697  matunitlindflem1  37954  unichnidl  38369  linepsubN  40215  pmapsub  40231  cdlemkid4  41397  hbtlem2  43573  2reu8i  47576  ply1mulgsumlem2  48878