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  1361  ad5ant125  1368  ad5ant2345  1372  peano5  7849  oelim  8475  lemul12a  12016  uzwo  12846  elfznelfzo  13709  injresinj  13725  swrdswrd  14646  2cshwcshw  14767  dvdsprmpweqle  16833  catidd  17621  grpinveu  18888  2ndcctbss  23375  rusgrnumwwlks  29954  erclwwlktr  30001  wwlksext2clwwlk  30036  erclwwlkntr  30050  grpoinveu  30498  spansncvi  31631  sumdmdii  32394  relowlpssretop  37345  matunitlindflem1  37603  unichnidl  38018  linepsubN  39739  pmapsub  39755  cdlemkid4  40921  hbtlem2  43106  2reu8i  47107  ply1mulgsumlem2  48369