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  7835  oelim  8461  lemul12a  11999  uzwo  12824  elfznelfzo  13689  injresinj  13707  swrdswrd  14628  2cshwcshw  14748  dvdsprmpweqle  16814  catidd  17603  grpinveu  18904  2ndcctbss  23399  rusgrnumwwlks  30050  erclwwlktr  30097  wwlksext2clwwlk  30132  erclwwlkntr  30146  grpoinveu  30594  spansncvi  31727  sumdmdii  32490  relowlpssretop  37569  matunitlindflem1  37817  unichnidl  38232  linepsubN  40022  pmapsub  40038  cdlemkid4  41204  hbtlem2  43376  2reu8i  47369  ply1mulgsumlem2  48643