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  1361  ad5ant125  1368  ad5ant2345  1372  peano5  7872  oelim  8501  lemul12a  12047  uzwo  12877  elfznelfzo  13740  injresinj  13756  swrdswrd  14677  2cshwcshw  14798  dvdsprmpweqle  16864  catidd  17648  grpinveu  18913  2ndcctbss  23349  rusgrnumwwlks  29911  erclwwlktr  29958  wwlksext2clwwlk  29993  erclwwlkntr  30007  grpoinveu  30455  spansncvi  31588  sumdmdii  32351  relowlpssretop  37359  matunitlindflem1  37617  unichnidl  38032  linepsubN  39753  pmapsub  39769  cdlemkid4  40935  hbtlem2  43120  2reu8i  47118  ply1mulgsumlem2  48380