Theorem imp41 416

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  ad4ant13OLD  758  ad4ant14OLD  760  ad4ant23OLD  762  ad4ant24OLD  764  ad5ant13OLD  768  ad5ant14OLD  770  ad5ant15OLD  772  ad5ant23OLD  774  ad5ant24OLD  776  ad5ant25OLD  778  ad4ant123OLD  1214  ad4ant124OLD  1216  ad4ant134OLD  1218  ad4ant234OLD  1220  3anassrs  1469  ad5ant245OLD  1471  ad5ant234OLD  1473  ad5ant235OLD  1475  ad5ant123OLD  1477  ad5ant124OLD  1479  ad5ant125  1480  ad5ant125OLD  1481  ad5ant134OLD  1483  ad5ant135OLD  1485  ad5ant145OLD  1487  ad5ant2345  1489  peano5  7287  oelim  7819  lemul12a  11135  uzwo  11952  elfznelfzo  12781  injresinj  12797  swrdswrd  13692  2cshwcshw  13854  dvdsprmpweqle  15869  catidd  16606  grpinveu  17723  2ndcctbss  21538  rusgrnumwwlks  27199  rusgrnumwwlksOLD  27200  erclwwlktr  27258  erclwwlkntr  27323  grpoinveu  27830  spansncvi  28967  sumdmdii  29730  relowlpssretop  33645  matunitlindflem1  33829  unichnidl  34252  linepsubN  35708  pmapsub  35724  cdlemkid4  36890  hbtlem2  38371  ply1mulgsumlem2  42844