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  7844  oelim  8469  lemul12a  12013  uzwo  12861  elfznelfzo  13728  injresinj  13746  swrdswrd  14667  2cshwcshw  14787  dvdsprmpweqle  16857  catidd  17646  grpinveu  18950  2ndcctbss  23420  rusgrnumwwlks  30045  erclwwlktr  30092  wwlksext2clwwlk  30127  erclwwlkntr  30141  grpoinveu  30590  spansncvi  31723  sumdmdii  32486  relowlpssretop  37680  matunitlindflem1  37937  unichnidl  38352  linepsubN  40198  pmapsub  40214  cdlemkid4  41380  hbtlem2  43552  2reu8i  47561  ply1mulgsumlem2  48863