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

This theorem is referenced by:  3anassrs  1358  ad5ant125  1364  ad5ant2345  1368  peano5  7727  peano5OLD  7728  oelim  8340  lemul12a  11816  uzwo  12633  elfznelfzo  13473  injresinj  13489  swrdswrd  14399  2cshwcshw  14519  dvdsprmpweqle  16568  catidd  17370  grpinveu  18595  2ndcctbss  22587  rusgrnumwwlks  28318  erclwwlktr  28365  wwlksext2clwwlk  28400  erclwwlkntr  28414  grpoinveu  28860  spansncvi  29993  sumdmdii  30756  relowlpssretop  35514  matunitlindflem1  35752  unichnidl  36168  linepsubN  37745  pmapsub  37761  cdlemkid4  38927  hbtlem2  40929  2reu8i  44556  ply1mulgsumlem2  45680