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  7833  oelim  8459  lemul12a  11997  uzwo  12822  elfznelfzo  13687  injresinj  13705  swrdswrd  14626  2cshwcshw  14746  dvdsprmpweqle  16812  catidd  17601  grpinveu  18902  2ndcctbss  23397  rusgrnumwwlks  29999  erclwwlktr  30046  wwlksext2clwwlk  30081  erclwwlkntr  30095  grpoinveu  30543  spansncvi  31676  sumdmdii  32439  relowlpssretop  37508  matunitlindflem1  37756  unichnidl  38171  linepsubN  39951  pmapsub  39967  cdlemkid4  41133  hbtlem2  43308  2reu8i  47301  ply1mulgsumlem2  48575