Theorem 3anassrs 1360

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 1354	. 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  3211  euotd  5532  dfgrp3e  19080  kerf1ghm  19287  psgndif  21643  neiptopnei  23161  neitr  23209  neitx  23636  cnextcn  24096  utoptop  24264  ustuqtoplem  24269  ustuqtop1  24271  utopsnneiplem  24277  utop3cls  24281  neipcfilu  24326  xmetpsmet  24379  metustsym  24589  grporcan  30550  disjdsct  32714  xrofsup  32774  omndmul2  33062  archirngz  33169  archiabllem1  33173  archiabllem2c  33175  reofld  33337  prmidl2  33434  pstmfval  33842  tpr2rico  33858  esumpcvgval  34042  esumcvg  34050  esum2d  34057  voliune  34193  signsply0  34528  signstfvneq0  34549  f1o2d2  42228