Theorem imp41 431

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3anassrs  1381  ad5ant125OLD  1391  ad5ant2345  1397  peano5  7912  oelim  8553  lemul12a  12185  uzwo  13048  elfznelfzo  13918  injresinj  13936  swrdswrd  14865  2cshwcshw  14987  dvdsprmpweqle  17076  catidd  17866  grpinveu  19197  unichnlidl  21528  matunitlindflem1  23006  2ndcctbss  23786  rusgrnumwwlks  30578  erclwwlktr  30625  wwlksext2clwwlk  30660  erclwwlkntr  30674  grpoinveu  31133  spansncvi  32266  sumdmdii  33029  relowlpssretop  38427  unichnidl  39105  linepsubN  40949  pmapsub  40965  cdlemkid4  42131  hbtlem2  44266  2reu8i  48323  ply1mulgsumlem2  49638