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  7823  oelim  8449  lemul12a  11979  uzwo  12809  elfznelfzo  13673  injresinj  13691  swrdswrd  14612  2cshwcshw  14732  dvdsprmpweqle  16798  catidd  17586  grpinveu  18887  2ndcctbss  23370  rusgrnumwwlks  29955  erclwwlktr  30002  wwlksext2clwwlk  30037  erclwwlkntr  30051  grpoinveu  30499  spansncvi  31632  sumdmdii  32395  relowlpssretop  37408  matunitlindflem1  37666  unichnidl  38081  linepsubN  39861  pmapsub  39877  cdlemkid4  41043  hbtlem2  43227  2reu8i  47223  ply1mulgsumlem2  48498