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  3179  euotd  5458  dfgrp3e  18961  kerf1ghm  19167  omndmul2  20053  psgndif  21548  neiptopnei  23067  neitr  23115  neitx  23542  cnextcn  24002  utoptop  24169  ustuqtoplem  24174  ustuqtop1  24176  utopsnneiplem  24182  utop3cls  24186  neipcfilu  24230  xmetpsmet  24283  metustsym  24490  grporcan  30519  disjdsct  32708  xrofsup  32775  archirngz  33199  archiabllem1  33203  archiabllem2c  33205  reofld  33352  prmidl2  33450  pstmfval  33981  tpr2rico  33997  esumpcvgval  34163  esumcvg  34171  esum2d  34178  voliune  34314  signsply0  34636  signstfvneq0  34657  f1o2d2  42404