Theorem imp41 430

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3anassrs  1379  ad5ant125OLD  1389  ad5ant2345  1395  peano5  7890  oelim  8519  lemul12a  12073  uzwo  12935  elfznelfzo  13802  injresinj  13820  swrdswrd  14742  2cshwcshw  14862  dvdsprmpweqle  16946  catidd  17736  grpinveu  19041  unichnlidl  21340  2ndcctbss  23581  rusgrnumwwlks  30267  erclwwlktr  30314  wwlksext2clwwlk  30349  erclwwlkntr  30363  grpoinveu  30812  spansncvi  31945  sumdmdii  32708  relowlpssretop  37898  matunitlindflem1  38155  unichnidl  38570  linepsubN  40416  pmapsub  40432  cdlemkid4  41598  hbtlem2  43743  2reu8i  47739  ply1mulgsumlem2  49052