Theorem imp41 617

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  3anassrs  1282  ad4ant13  1284  ad4ant14  1285  ad4ant123  1286  ad4ant124  1287  ad4ant134  1288  ad4ant23  1289  ad4ant24  1290  ad4ant234  1291  ad5ant13  1293  ad5ant14  1294  ad5ant15  1295  ad5ant23  1296  ad5ant24  1297  ad5ant25  1298  ad5ant245  1299  ad5ant234  1300  ad5ant235  1301  ad5ant123  1302  ad5ant124  1303  ad5ant125  1304  ad5ant134  1305  ad5ant135  1306  ad5ant145  1307  ad5ant2345  1309  peano5  6981  oelim  7501  lemul12a  10760  uzwo  11627  elfznelfzo  12439  injresinj  12451  swrdswrd  13312  2cshwcshw  13422  dvdsprmpweqle  15428  catidd  16164  grpinveu  17279  2ndcctbss  21068  erclwwlktr  26343  erclwwlkntr  26355  el2spthonot  26397  rusgranumwlks  26483  2pthfrgra  26538  frgrancvvdeqlemB  26565  2spotiundisj  26589  usg2spot2nb  26592  grpoinveu  26757  spansncvi  27895  sumdmdii  28658  relowlpssretop  32388  matunitlindflem1  32575  unichnidl  33000  linepsubN  34056  pmapsub  34072  cdlemkid4  35240  hbtlem2  36713  rusgrnumwwlks  41177  erclwwlkstr  41243  erclwwlksntr  41255  frgrncvvdeqlemB  41477  ply1mulgsumlem2  41969