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  1362  ad5ant125  1369  ad5ant2345  1373  peano5  7845  oelim  8471  lemul12a  12011  uzwo  12836  elfznelfzo  13701  injresinj  13719  swrdswrd  14640  2cshwcshw  14760  dvdsprmpweqle  16826  catidd  17615  grpinveu  18916  2ndcctbss  23411  rusgrnumwwlks  30062  erclwwlktr  30109  wwlksext2clwwlk  30144  erclwwlkntr  30158  grpoinveu  30607  spansncvi  31740  sumdmdii  32503  relowlpssretop  37619  matunitlindflem1  37867  unichnidl  38282  linepsubN  40128  pmapsub  40144  cdlemkid4  41310  hbtlem2  43481  2reu8i  47473  ply1mulgsumlem2  48747