Theorem imp41 429

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  3anassrs  1374  ad5ant125OLD  1383  ad5ant2345  1389  peano5  7874  oelim  8503  lemul12a  12049  uzwo  12912  elfznelfzo  13779  injresinj  13797  swrdswrd  14718  2cshwcshw  14838  dvdsprmpweqle  16922  catidd  17712  grpinveu  19016  2ndcctbss  23515  rusgrnumwwlks  30177  erclwwlktr  30224  wwlksext2clwwlk  30259  erclwwlkntr  30273  grpoinveu  30722  spansncvi  31855  sumdmdii  32618  relowlpssretop  37858  matunitlindflem1  38115  unichnidl  38530  linepsubN  40376  pmapsub  40392  cdlemkid4  41558  hbtlem2  43701  2reu8i  47707  ply1mulgsumlem2  49009