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 427	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ralrimivvva  3204  euotd  5514  dfgrp3e  18923  kerf1ghm  20282  psgndif  21155  neiptopnei  22636  neitr  22684  neitx  23111  cnextcn  23571  utoptop  23739  ustuqtoplem  23744  ustuqtop1  23746  utopsnneiplem  23752  utop3cls  23756  neipcfilu  23801  xmetpsmet  23854  metustsym  24064  grporcan  29771  disjdsct  31924  xrofsup  31980  omndmul2  32230  archirngz  32335  archiabllem1  32339  archiabllem2c  32341  reofld  32459  prmidl2  32559  pstmfval  32876  tpr2rico  32892  esumpcvgval  33076  esumcvg  33084  esum2d  33091  voliune  33227  signsply0  33562  signstfvneq0  33583  f1o2d2  41055