Theorem 3anassrs 1358

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 1352	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
3	2	imp41 425	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ralrimivvva  3199  euotd  5510  dfgrp3e  18990  kerf1ghm  19195  psgndif  21528  neiptopnei  23030  neitr  23078  neitx  23505  cnextcn  23965  utoptop  24133  ustuqtoplem  24138  ustuqtop1  24140  utopsnneiplem  24146  utop3cls  24150  neipcfilu  24195  xmetpsmet  24248  metustsym  24458  grporcan  30322  disjdsct  32477  xrofsup  32532  omndmul2  32787  archirngz  32892  archiabllem1  32896  archiabllem2c  32898  reofld  33051  prmidl2  33152  pstmfval  33492  tpr2rico  33508  esumpcvgval  33692  esumcvg  33700  esum2d  33707  voliune  33843  signsply0  34178  signstfvneq0  34199  f1o2d2  41715