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  1360  ad5ant125  1366  ad5ant2345  1370  peano5  7932  peano5OLD  7933  oelim  8590  lemul12a  12152  uzwo  12976  elfznelfzo  13822  injresinj  13838  swrdswrd  14753  2cshwcshw  14874  dvdsprmpweqle  16933  catidd  17738  grpinveu  19014  2ndcctbss  23484  rusgrnumwwlks  30007  erclwwlktr  30054  wwlksext2clwwlk  30089  erclwwlkntr  30103  grpoinveu  30551  spansncvi  31684  sumdmdii  32447  relowlpssretop  37330  matunitlindflem1  37576  unichnidl  37991  linepsubN  39709  pmapsub  39725  cdlemkid4  40891  hbtlem2  43081  2reu8i  47028  ply1mulgsumlem2  48116