Theorem imp41 427

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3anassrs  1361  ad5ant125  1367  ad5ant2345  1371  peano5  7884  peano5OLD  7885  oelim  8534  lemul12a  12072  uzwo  12895  elfznelfzo  13737  injresinj  13753  swrdswrd  14655  2cshwcshw  14776  dvdsprmpweqle  16819  catidd  17624  grpinveu  18859  2ndcctbss  22959  rusgrnumwwlks  29228  erclwwlktr  29275  wwlksext2clwwlk  29310  erclwwlkntr  29324  grpoinveu  29772  spansncvi  30905  sumdmdii  31668  relowlpssretop  36245  matunitlindflem1  36484  unichnidl  36899  linepsubN  38623  pmapsub  38639  cdlemkid4  39805  hbtlem2  41866  2reu8i  45821  ply1mulgsumlem2  47068