Theorem imp41 427

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3anassrs  1360  ad5ant125  1366  ad5ant2345  1370  peano5  7772  peano5OLD  7773  oelim  8395  lemul12a  11879  uzwo  12697  elfznelfzo  13538  injresinj  13554  swrdswrd  14463  2cshwcshw  14583  dvdsprmpweqle  16632  catidd  17434  grpinveu  18659  2ndcctbss  22651  rusgrnumwwlks  28384  erclwwlktr  28431  wwlksext2clwwlk  28466  erclwwlkntr  28480  grpoinveu  28926  spansncvi  30059  sumdmdii  30822  relowlpssretop  35579  matunitlindflem1  35817  unichnidl  36233  linepsubN  37808  pmapsub  37824  cdlemkid4  38990  hbtlem2  40987  2reu8i  44663  ply1mulgsumlem2  45786