Theorem imp41 428

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3anassrs  1355  ad5ant125  1361  ad5ant2345  1365  peano5  7597  oelim  8151  lemul12a  11490  uzwo  12303  elfznelfzo  13134  injresinj  13150  swrdswrd  14059  2cshwcshw  14179  dvdsprmpweqle  16214  catidd  16943  grpinveu  18130  2ndcctbss  22055  rusgrnumwwlks  27745  erclwwlktr  27792  wwlksext2clwwlk  27828  erclwwlkntr  27842  grpoinveu  28288  spansncvi  29421  sumdmdii  30184  relowlpssretop  34637  matunitlindflem1  34880  unichnidl  35301  linepsubN  36880  pmapsub  36896  cdlemkid4  38062  hbtlem2  39715  2reu8i  43303  ply1mulgsumlem2  44432