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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  ralrimivvva  3203  euotd  5513  dfgrp3e  18925  kerf1ghm  20286  psgndif  21161  neiptopnei  22643  neitr  22691  neitx  23118  cnextcn  23578  utoptop  23746  ustuqtoplem  23751  ustuqtop1  23753  utopsnneiplem  23759  utop3cls  23763  neipcfilu  23808  xmetpsmet  23861  metustsym  24071  grporcan  29809  disjdsct  31962  xrofsup  32018  omndmul2  32271  archirngz  32376  archiabllem1  32380  archiabllem2c  32382  reofld  32500  prmidl2  32604  pstmfval  32945  tpr2rico  32961  esumpcvgval  33145  esumcvg  33153  esum2d  33160  voliune  33296  signsply0  33631  signstfvneq0  33652  f1o2d2  41141