Theorem 3anassrs 1367

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ralrimivvva  3185  euotd  5454  mpof1o2d  8065  dfgrp3e  19007  kerf1ghm  19213  omndmul2  20099  psgndif  21577  neiptopnei  23115  neitr  23163  neitx  23590  cnextcn  24050  utoptop  24217  ustuqtoplem  24222  ustuqtop1  24224  utopsnneiplem  24230  utop3cls  24234  neipcfilu  24278  xmetpsmet  24331  metustsym  24538  grporcan  30607  disjdsct  32795  xrofsup  32859  archirngz  33270  archiabllem1  33274  archiabllem2c  33276  reofld  33426  prmidl2  33524  pstmfval  34080  tpr2rico  34096  esumpcvgval  34262  esumcvg  34270  esum2d  34277  voliune  34413  signsply0  34735  signstfvneq0  34756