Theorem imp41 426

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  3anassrs  1360  ad5ant125  1366  ad5ant2345  1370  peano5  7835  peano5OLD  7836  oelim  8485  lemul12a  12022  uzwo  12845  elfznelfzo  13687  injresinj  13703  swrdswrd  14605  2cshwcshw  14726  dvdsprmpweqle  16769  catidd  17574  grpinveu  18799  2ndcctbss  22843  rusgrnumwwlks  28982  erclwwlktr  29029  wwlksext2clwwlk  29064  erclwwlkntr  29078  grpoinveu  29524  spansncvi  30657  sumdmdii  31420  relowlpssretop  35908  matunitlindflem1  36147  unichnidl  36563  linepsubN  38288  pmapsub  38304  cdlemkid4  39470  hbtlem2  41509  2reu8i  45465  ply1mulgsumlem2  46588