Theorem 3anassrs 1359

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 1353	. 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  3203  euotd  5523  dfgrp3e  19071  kerf1ghm  19278  psgndif  21638  neiptopnei  23156  neitr  23204  neitx  23631  cnextcn  24091  utoptop  24259  ustuqtoplem  24264  ustuqtop1  24266  utopsnneiplem  24272  utop3cls  24276  neipcfilu  24321  xmetpsmet  24374  metustsym  24584  grporcan  30547  disjdsct  32718  xrofsup  32778  omndmul2  33072  archirngz  33179  archiabllem1  33183  archiabllem2c  33185  reofld  33352  prmidl2  33449  pstmfval  33857  tpr2rico  33873  esumpcvgval  34059  esumcvg  34067  esum2d  34074  voliune  34210  signsply0  34545  signstfvneq0  34566  f1o2d2  42253