Theorem imp41 431

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3anassrs  1381  ad5ant125OLD  1391  ad5ant2345  1397  peano5  7896  oelim  8525  lemul12a  12090  uzwo  12953  elfznelfzo  13821  injresinj  13839  swrdswrd  14766  2cshwcshw  14888  dvdsprmpweqle  16970  catidd  17760  grpinveu  19087  unichnlidl  21414  2ndcctbss  23665  rusgrnumwwlks  30395  erclwwlktr  30442  wwlksext2clwwlk  30477  erclwwlkntr  30491  grpoinveu  30944  spansncvi  32077  sumdmdii  32840  relowlpssretop  38069  matunitlindflem1  38326  unichnidl  38742  linepsubN  40586  pmapsub  40602  cdlemkid4  41768  hbtlem2  43911  2reu8i  47910  ply1mulgsumlem2  49226