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

This theorem is referenced by:  3anassrs  1361  ad5ant125  1368  ad5ant2345  1372  peano5  7869  oelim  8498  lemul12a  12040  uzwo  12870  elfznelfzo  13733  injresinj  13749  swrdswrd  14670  2cshwcshw  14791  dvdsprmpweqle  16857  catidd  17641  grpinveu  18906  2ndcctbss  23342  rusgrnumwwlks  29904  erclwwlktr  29951  wwlksext2clwwlk  29986  erclwwlkntr  30000  grpoinveu  30448  spansncvi  31581  sumdmdii  32344  relowlpssretop  37352  matunitlindflem1  37610  unichnidl  38025  linepsubN  39746  pmapsub  39762  cdlemkid4  40928  hbtlem2  43113  2reu8i  47114  ply1mulgsumlem2  48376