Theorem 3anassrs 1381

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ralrimivvva  3208  euotd  5490  mpof1o2d  8123  dfgrp3e  19163  kerf1ghm  19374  omndmul2  20260  prmidl2  21529  psgndif  21815  neiptopnei  23357  neitr  23405  neitx  23833  cnextcn  24293  utoptop  24460  ustuqtoplem  24465  ustuqtop1  24467  utopsnneiplem  24473  utop3cls  24477  neipcfilu  24521  xmetpsmet  24574  metustsym  24781  grporcan  30999  disjdsct  33175  xrofsup  33238  archirngz  33629  archiabllem1  33633  archiabllem2c  33635  reofld  33783  pstmfval  34406  tpr2rico  34422  esumpcvgval  34588  esumcvg  34596  esum2d  34603  voliune  34740  signsply0  35059  signstfvneq0  35080