Theorem 3anassrs 1362

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

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

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 1089

This theorem is referenced by:  ralrimivvva  3184  euotd  5469  dfgrp3e  18982  kerf1ghm  19188  omndmul2  20074  psgndif  21569  neiptopnei  23088  neitr  23136  neitx  23563  cnextcn  24023  utoptop  24190  ustuqtoplem  24195  ustuqtop1  24197  utopsnneiplem  24203  utop3cls  24207  neipcfilu  24251  xmetpsmet  24304  metustsym  24511  grporcan  30605  disjdsct  32792  xrofsup  32857  archirngz  33282  archiabllem1  33286  archiabllem2c  33288  reofld  33435  prmidl2  33533  pstmfval  34073  tpr2rico  34089  esumpcvgval  34255  esumcvg  34263  esum2d  34270  voliune  34406  signsply0  34728  signstfvneq0  34749  f1o2d2  42602