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  7894  oelim  8551  lemul12a  12104  uzwo  12932  elfznelfzo  13793  injresinj  13809  swrdswrd  14728  2cshwcshw  14849  dvdsprmpweqle  16911  catidd  17697  grpinveu  18962  2ndcctbss  23398  rusgrnumwwlks  29961  erclwwlktr  30008  wwlksext2clwwlk  30043  erclwwlkntr  30057  grpoinveu  30505  spansncvi  31638  sumdmdii  32401  relowlpssretop  37387  matunitlindflem1  37645  unichnidl  38060  linepsubN  39776  pmapsub  39792  cdlemkid4  40958  hbtlem2  43115  2reu8i  47109  ply1mulgsumlem2  48330