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  7915  oelim  8572  lemul12a  12125  uzwo  12953  elfznelfzo  13811  injresinj  13827  swrdswrd  14743  2cshwcshw  14864  dvdsprmpweqle  16924  catidd  17723  grpinveu  18992  2ndcctbss  23463  rusgrnumwwlks  29994  erclwwlktr  30041  wwlksext2clwwlk  30076  erclwwlkntr  30090  grpoinveu  30538  spansncvi  31671  sumdmdii  32434  relowlpssretop  37365  matunitlindflem1  37623  unichnidl  38038  linepsubN  39754  pmapsub  39770  cdlemkid4  40936  hbtlem2  43136  2reu8i  47125  ply1mulgsumlem2  48304