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  3182  euotd  5461  dfgrp3e  18970  kerf1ghm  19176  omndmul2  20062  psgndif  21557  neiptopnei  23076  neitr  23124  neitx  23551  cnextcn  24011  utoptop  24178  ustuqtoplem  24183  ustuqtop1  24185  utopsnneiplem  24191  utop3cls  24195  neipcfilu  24239  xmetpsmet  24292  metustsym  24499  grporcan  30593  disjdsct  32782  xrofsup  32847  archirngz  33271  archiabllem1  33275  archiabllem2c  33277  reofld  33424  prmidl2  33522  pstmfval  34053  tpr2rico  34069  esumpcvgval  34235  esumcvg  34243  esum2d  34250  voliune  34386  signsply0  34708  signstfvneq0  34729  f1o2d2  42489