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

This theorem is referenced by:  3anassrs  1353  ad5ant125  1359  ad5ant2345  1363  peano5  7468  oelim  8017  lemul12a  11352  uzwo  12164  elfznelfzo  12996  injresinj  13012  swrdswrd  13907  2cshwcshw  14027  dvdsprmpweqle  16055  catidd  16784  grpinveu  17899  2ndcctbss  21751  rusgrnumwwlks  27439  erclwwlktr  27486  erclwwlkntr  27536  grpoinveu  27983  spansncvi  29116  sumdmdii  29879  relowlpssretop  34197  matunitlindflem1  34440  unichnidl  34862  linepsubN  36440  pmapsub  36456  cdlemkid4  37622  hbtlem2  39230  2reu8i  42850  ply1mulgsumlem2  43943