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  1381  ad5ant125OLD  1391  ad5ant2345  1397  peano5  7886  oelim  8515  lemul12a  12068  uzwo  12930  elfznelfzo  13798  injresinj  13816  swrdswrd  14738  2cshwcshw  14858  dvdsprmpweqle  16941  catidd  17731  grpinveu  19036  unichnlidl  21362  2ndcctbss  23612  rusgrnumwwlks  30326  erclwwlktr  30373  wwlksext2clwwlk  30408  erclwwlkntr  30422  grpoinveu  30871  spansncvi  32004  sumdmdii  32767  relowlpssretop  38030  matunitlindflem1  38287  unichnidl  38702  linepsubN  40546  pmapsub  40562  cdlemkid4  41728  hbtlem2  43871  2reu8i  47870  ply1mulgsumlem2  49187