Theorem 3anassrs 1361

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
3anassrs.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
3anassrs	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3anassrs

Step	Hyp	Ref	Expression
1		3anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
2	1	3exp2 1355	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
3	2	imp41 425	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  ralrimivvva  3175  euotd  5460  dfgrp3e  18938  kerf1ghm  19145  omndmul2  20031  psgndif  21528  neiptopnei  23036  neitr  23084  neitx  23511  cnextcn  23971  utoptop  24139  ustuqtoplem  24144  ustuqtop1  24146  utopsnneiplem  24152  utop3cls  24156  neipcfilu  24200  xmetpsmet  24253  metustsym  24460  grporcan  30481  disjdsct  32664  xrofsup  32729  archirngz  33150  archiabllem1  33154  archiabllem2c  33156  reofld  33300  prmidl2  33397  pstmfval  33882  tpr2rico  33898  esumpcvgval  34064  esumcvg  34072  esum2d  34079  voliune  34215  signsply0  34538  signstfvneq0  34559  f1o2d2  42226