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  7826  oelim  8452  lemul12a  11982  uzwo  12812  elfznelfzo  13675  injresinj  13691  swrdswrd  14611  2cshwcshw  14732  dvdsprmpweqle  16798  catidd  17586  grpinveu  18853  2ndcctbss  23340  rusgrnumwwlks  29919  erclwwlktr  29966  wwlksext2clwwlk  30001  erclwwlkntr  30015  grpoinveu  30463  spansncvi  31596  sumdmdii  32359  relowlpssretop  37342  matunitlindflem1  37600  unichnidl  38015  linepsubN  39735  pmapsub  39751  cdlemkid4  40917  hbtlem2  43101  2reu8i  47101  ply1mulgsumlem2  48376