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  1367  ad5ant125  1374  ad5ant2345  1378  peano5  7833  oelim  8459  lemul12a  12004  uzwo  12852  elfznelfzo  13719  injresinj  13737  swrdswrd  14658  2cshwcshw  14778  dvdsprmpweqle  16848  catidd  17637  grpinveu  18941  2ndcctbss  23438  rusgrnumwwlks  30063  erclwwlktr  30110  wwlksext2clwwlk  30145  erclwwlkntr  30159  grpoinveu  30608  spansncvi  31741  sumdmdii  32504  relowlpssretop  37726  matunitlindflem1  37983  unichnidl  38398  linepsubN  40244  pmapsub  40260  cdlemkid4  41426  hbtlem2  43569  2reu8i  47576  ply1mulgsumlem2  48878